Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga45_44_sat_pb.cnf.cr.opb |
MD5SUM | c501a04dd091dbe678ec2743021adc30 |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 46 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 15.2037 |
Number of variables | 2970 |
Total number of constraints | 2113 |
Number of constraints which are clauses | 2024 |
Number of constraints which are cardinality constraints (but not clauses) | 89 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 22 |
Maximum length of a constraint | 45 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc17 THE 2005-04-14 03:35:29 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4568 boxname=wulflinc17 idbench=56 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c501a04dd091dbe678ec2743021adc30 /oldhome/oroussel/tmp/wulflinc17/normalized-fpga45_44_sat_pb.cnf.cr.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc17/normalized-fpga45_44_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc17/normalized-fpga45_44_sat_pb.cnf.cr.opb IDLAUNCH: 4568 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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: 818968 kB Buffers: 36012 kB Cached: 144668 kB SwapCached: 2376 kB Active: 59416 kB Inactive: 126636 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 818716 kB SwapTotal: 2097892 kB SwapFree: 2095516 kB Dirty: 28 kB Writeback: 0 kB Mapped: 7036 kB Slab: 23888 kB Committed_AS: 63708 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 03:55:31 (client local time) WITH STATUS 0 IN 1200.24 SECONDS stats: 4568 7 1200.24 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 2113 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ c ---[ 88]---> BDD-cost: 85 c ---[ 87]---> BDD-cost: 85 c ---[ 86]---> BDD-cost: 85 c ---[ 85]---> BDD-cost: 85 c ---[ 84]---> BDD-cost: 85 c ---[ 83]---> BDD-cost: 85 c ---[ 82]---> BDD-cost: 85 c ---[ 81]---> BDD-cost: 85 c ---[ 80]---> BDD-cost: 85 c ---[ 79]---> BDD-cost: 85 c ---[ 78]---> BDD-cost: 85 c ---[ 77]---> BDD-cost: 85 c ---[ 76]---> BDD-cost: 85 c ---[ 75]---> BDD-cost: 85 c ---[ 74]---> BDD-cost: 85 c ---[ 73]---> BDD-cost: 85 c ---[ 72]---> BDD-cost: 85 c ---[ 71]---> BDD-cost: 85 c ---[ 70]---> BDD-cost: 85 c ---[ 69]---> BDD-cost: 85 c ---[ 68]---> BDD-cost: 85 c ---[ 67]---> BDD-cost: 85 c ---[ 66]---> BDD-cost: 85 c ---[ 65]---> BDD-cost: 85 c ---[ 64]---> BDD-cost: 85 c ---[ 63]---> BDD-cost: 85 c ---[ 62]---> BDD-cost: 85 c ---[ 61]---> BDD-cost: 85 c ---[ 60]---> BDD-cost: 85 c ---[ 59]---> BDD-cost: 85 c ---[ 58]---> BDD-cost: 85 c ---[ 57]---> BDD-cost: 85 c ---[ 56]---> BDD-cost: 85 c ---[ 55]---> BDD-cost: 85 c ---[ 54]---> BDD-cost: 85 c ---[ 53]---> BDD-cost: 85 c ---[ 52]---> BDD-cost: 85 c ---[ 51]---> BDD-cost: 85 c ---[ 50]---> BDD-cost: 85 c ---[ 49]---> BDD-cost: 85 c ---[ 48]---> BDD-cost: 85 c ---[ 47]---> BDD-cost: 85 c ---[ 46]---> BDD-cost: 85 c ---[ 45]---> BDD-cost: 85 c ---[ 44]---> BDD-cost: 85 c ---[ 43]---> BDD-cost: 41 c ---[ 42]---> BDD-cost: 41 c ---[ 41]---> BDD-cost: 41 c ---[ 40]---> BDD-cost: 41 c ---[ 39]---> BDD-cost: 41 c ---[ 38]---> BDD-cost: 41 c ---[ 37]---> BDD-cost: 41 c ---[ 36]---> BDD-cost: 41 c ---[ 35]---> BDD-cost: 41 c ---[ 34]---> BDD-cost: 41 c ---[ 33]---> BDD-cost: 41 c ---[ 32]---> BDD-cost: 41 c ---[ 31]---> BDD-cost: 41 c ---[ 30]---> BDD-cost: 41 c ---[ 29]---> BDD-cost: 41 c ---[ 28]---> BDD-cost: 41 c ---[ 27]---> BDD-cost: 41 c ---[ 26]---> BDD-cost: 41 c ---[ 25]---> BDD-cost: 41 c ---[ 24]---> BDD-cost: 41 c ---[ 23]---> BDD-cost: 41 c ---[ 22]---> BDD-cost: 41 c ---[ 21]---> BDD-cost: 43 c ---[ 20]---> BDD-cost: 43 c ---[ 19]---> BDD-cost: 43 c ---[ 18]---> BDD-cost: 43 c ---[ 17]---> BDD-cost: 43 c ---[ 16]---> BDD-cost: 43 c ---[ 15]---> BDD-cost: 43 c ---[ 14]---> BDD-cost: 43 c ---[ 13]---> BDD-cost: 43 c ---[ 12]---> BDD-cost: 43 c ---[ 11]---> BDD-cost: 43 c ---[ 10]---> BDD-cost: 43 c ---[ 9]---> BDD-cost: 43 c ---[ 8]---> BDD-cost: 43 c ---[ 7]---> BDD-cost: 43 c ---[ 6]---> BDD-cost: 43 c ---[ 5]---> BDD-cost: 43 c ---[ 4]---> BDD-cost: 43 c ---[ 3]---> BDD-cost: 43 c ---[ 2]---> BDD-cost: 43 c ---[ 1]---> BDD-cost: 43 c ---[ 0]---> BDD-cost: 43 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 27152 117142 | 9050 0 0 nan | 0.000 % | c | 102 | 27048 116832 | 9955 54 3075 56.9 | 1.273 % | c | 253 | 26773 116007 | 10950 53 1128 21.3 | 1.909 % | c | 478 | 26263 114477 | 12045 71 1254 17.7 | 3.089 % | c | 815 | 25673 112707 | 13250 172 16677 97.0 | 4.454 % | c | 1323 | 25423 111957 | 14575 568 123633 217.7 | 5.033 % | c | 2082 | 25193 111267 | 16032 1233 352448 285.8 | 5.565 % | c | 3221 | 24468 109092 | 17635 2100 560481 266.9 | 7.243 % | c | 4929 | 23098 104982 | 19399 3282 881270 268.5 | 10.413 % | c | 7491 | 21913 101427 | 21339 5388 1568418 291.1 | 13.155 % | c | 11335 | 20169 96197 | 23473 8607 2534268 294.4 | 17.193 % | c | 17101 | 19249 93437 | 25820 14032 4396026 313.3 | 19.322 % | c | 25750 | 18000 89692 | 28402 22242 7137212 320.9 | 22.215 % | c | 38730 | 17046 86832 | 31243 15204 4652080 306.0 | 24.424 % | c | 58193 | 16771 86007 | 34367 34586 9838680 284.5 | 25.061 % | c | 87385 | 15861 83277 | 37804 39190 10464321 267.0 | 27.166 % | c | 131174 | 15446 82032 | 41584 21451 5442220 253.7 | 28.127 % | c | 196858 | 14883 80347 | 45742 21332 6447154 302.2 | 29.434 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.91 0.95 0.90 2/55 28341 Raw data (stat): 28341 (runsolver) R 28340 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481402018 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99928 s] Raw data (loadavg): 0.93 0.95 0.90 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 1650 0 0 0 995 3 0 0 25 0 1 0 481402018 8663040 1627 4294967295 134512640 134672761 3221224528 3221223632 134560005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2115 1628 603 41 0 2074 0 vsize: 8460 [startup+19.9999 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 1883 0 0 0 1994 4 0 0 25 0 1 0 481402018 9609216 1860 4294967295 134512640 134672761 3221224528 3221223708 134556590 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2346 1860 603 41 0 2305 0 vsize: 9384 [startup+29.9997 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 2568 0 0 0 2992 6 0 0 25 0 1 0 481402018 12439552 2545 4294967295 134512640 134672761 3221224528 3221223632 134559866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3037 2545 603 41 0 2996 0 vsize: 12148 [startup+40.0001 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 2834 0 0 0 3992 6 0 0 25 0 1 0 481402018 13512704 2811 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3299 2811 603 41 0 3258 0 vsize: 13196 [startup+49.9997 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 3237 0 0 0 4991 8 0 0 25 0 1 0 481402018 15134720 3214 4294967295 134512640 134672761 3221224528 3221223700 134556671 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3695 3214 603 41 0 3654 0 vsize: 14780 [startup+59.9996 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 3341 0 0 0 5990 8 0 0 25 0 1 0 481402018 15540224 3318 4294967295 134512640 134672761 3221224528 3221223680 134565110 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3794 3318 603 41 0 3753 0 vsize: 15176 [startup+69.9999 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 3628 0 0 0 6990 9 0 0 25 0 1 0 481402018 16756736 3605 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4091 3605 603 41 0 4050 0 vsize: 16364 [startup+79.9995 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 4540 0 0 0 7988 11 0 0 25 0 1 0 481402018 20537344 4517 4294967295 134512640 134672761 3221224528 3221223700 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5014 4517 603 41 0 4973 0 vsize: 20056 [startup+89.9994 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 4625 0 0 0 8988 11 0 0 25 0 1 0 481402018 20807680 4602 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5080 4602 603 41 0 5039 0 vsize: 20320 [startup+99.9987 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 5719 0 0 0 9985 14 0 0 25 0 1 0 481402018 25255936 5696 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6166 5696 603 41 0 6125 0 vsize: 24664 [startup+109.998 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 5912 0 0 0 10984 15 0 0 25 0 1 0 481402018 26066944 5889 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6364 5889 603 41 0 6323 0 vsize: 25456 [startup+119.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 6757 0 0 0 11982 17 0 0 25 0 1 0 481402018 29577216 6734 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7221 6734 603 41 0 7180 0 vsize: 28884 [startup+129.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 7339 0 0 0 12980 19 0 0 25 0 1 0 481402018 32026624 7316 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7819 7316 603 41 0 7778 0 vsize: 31276 [startup+139.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 7797 0 0 0 13980 20 0 0 25 0 1 0 481402018 33914880 7774 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8280 7774 603 41 0 8239 0 vsize: 33120 [startup+149.998 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 7979 0 0 0 14979 20 0 0 25 0 1 0 481402018 34590720 7956 4294967295 134512640 134672761 3221224528 3221223632 134560191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8445 7956 603 41 0 8404 0 vsize: 33780 [startup+159.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 8100 0 0 0 15979 21 0 0 25 0 1 0 481402018 35127296 8077 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8576 8077 603 41 0 8535 0 vsize: 34304 [startup+169.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 8737 0 0 0 16978 22 0 0 25 0 1 0 481402018 37695488 8714 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9203 8714 603 41 0 9162 0 vsize: 36812 [startup+179.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 9157 0 0 0 17977 23 0 0 25 0 1 0 481402018 39448576 9134 4294967295 134512640 134672761 3221224528 3221223632 134559981 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9631 9134 603 41 0 9590 0 vsize: 38524 [startup+189.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 9896 0 0 0 18975 25 0 0 25 0 1 0 481402018 42418176 9873 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10356 9873 603 41 0 10315 0 vsize: 41424 [startup+199.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 10098 0 0 0 19975 26 0 0 25 0 1 0 481402018 43229184 10075 4294967295 134512640 134672761 3221224528 3221223632 134560260 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10554 10075 603 41 0 10513 0 vsize: 42216 [startup+209.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 10476 0 0 0 20974 27 0 0 25 0 1 0 481402018 44847104 10453 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10949 10453 603 41 0 10908 0 vsize: 43796 [startup+219.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 11463 0 0 0 21971 30 0 0 25 0 1 0 481402018 48893952 11440 4294967295 134512640 134672761 3221224528 3221223700 134556651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11937 11440 603 41 0 11896 0 vsize: 47748 [startup+229.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 11798 0 0 0 22971 30 0 0 25 0 1 0 481402018 50245632 11775 4294967295 134512640 134672761 3221224528 3221223700 134556651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12267 11775 603 41 0 12226 0 vsize: 49068 [startup+239.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12056 0 0 0 23970 31 0 0 25 0 1 0 481402018 51322880 12033 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12530 12033 603 41 0 12489 0 vsize: 50120 [startup+249.997 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 24970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12859 12364 603 41 0 12818 0 vsize: 51436 [startup+259.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 25970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12859 12364 603 41 0 12818 0 vsize: 51436 [startup+269.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 26970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12859 12364 603 41 0 12818 0 vsize: 51436 [startup+279.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 27970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223700 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12859 12364 603 41 0 12818 0 vsize: 51436 [startup+289.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 28970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12859 12364 603 41 0 12818 0 vsize: 51436 [startup+299.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28343 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 29970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12859 12364 603 41 0 12818 0 vsize: 51436 [startup+309.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12387 0 0 0 30970 32 0 0 25 0 1 0 481402018 52670464 12364 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12859 12364 603 41 0 12818 0 vsize: 51436 [startup+319.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 12466 0 0 0 31970 32 0 0 25 0 1 0 481402018 52940800 12443 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12925 12443 603 41 0 12884 0 vsize: 51700 [startup+329.996 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 32968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13649 13155 603 41 0 13608 0 vsize: 54596 [startup+339.996 s] Raw data (loadavg): 1.07 0.99 0.91 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 33968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13649 13155 603 41 0 13608 0 vsize: 54596 [startup+349.996 s] Raw data (loadavg): 1.06 0.99 0.91 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 34968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13649 13155 603 41 0 13608 0 vsize: 54596 [startup+359.995 s] Raw data (loadavg): 1.05 0.99 0.91 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 35968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223700 134556602 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13649 13155 603 41 0 13608 0 vsize: 54596 [startup+369.996 s] Raw data (loadavg): 1.04 0.99 0.91 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 36968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13649 13155 603 41 0 13608 0 vsize: 54596 [startup+379.995 s] Raw data (loadavg): 1.04 0.99 0.91 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 37968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223700 134556643 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13649 13155 603 41 0 13608 0 vsize: 54596 [startup+389.995 s] Raw data (loadavg): 1.11 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 38968 34 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13649 13155 603 41 0 13608 0 vsize: 54596 [startup+399.995 s] Raw data (loadavg): 1.09 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13178 0 0 0 39968 35 0 0 25 0 1 0 481402018 55906304 13155 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13649 13155 603 41 0 13608 0 vsize: 54596 [startup+409.995 s] Raw data (loadavg): 1.08 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 13557 0 0 0 40967 36 0 0 25 0 1 0 481402018 57393152 13534 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14012 13534 603 41 0 13971 0 vsize: 56048 [startup+419.995 s] Raw data (loadavg): 1.07 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 41965 37 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223696 134561025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14734 14241 603 41 0 14693 0 vsize: 58936 [startup+429.995 s] Raw data (loadavg): 1.06 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 42965 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223700 134556680 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14734 14241 603 41 0 14693 0 vsize: 58936 [startup+439.995 s] Raw data (loadavg): 1.05 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 43966 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223712 134558771 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14734 14241 603 41 0 14693 0 vsize: 58936 [startup+449.995 s] Raw data (loadavg): 1.04 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 44966 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14734 14241 603 41 0 14693 0 vsize: 58936 [startup+459.995 s] Raw data (loadavg): 1.03 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 45966 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14734 14241 603 41 0 14693 0 vsize: 58936 [startup+469.995 s] Raw data (loadavg): 1.03 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 46966 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14734 14241 603 41 0 14693 0 vsize: 58936 [startup+479.995 s] Raw data (loadavg): 1.02 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 47966 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14734 14241 603 41 0 14693 0 vsize: 58936 [startup+489.996 s] Raw data (loadavg): 1.02 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 48966 38 0 0 25 0 1 0 481402018 60350464 14241 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14734 14241 603 41 0 14693 0 vsize: 58936 [startup+499.996 s] Raw data (loadavg): 1.02 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 49966 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14730 14241 603 41 0 14689 0 vsize: 58920 [startup+509.995 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 50966 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14730 14241 603 41 0 14689 0 vsize: 58920 [startup+519.996 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 51966 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14730 14241 603 41 0 14689 0 vsize: 58920 [startup+529.996 s] Raw data (loadavg): 1.01 1.00 0.92 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 52967 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14730 14241 603 41 0 14689 0 vsize: 58920 [startup+539.995 s] Raw data (loadavg): 1.08 1.02 0.93 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 53967 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14730 14241 603 41 0 14689 0 vsize: 58920 [startup+549.995 s] Raw data (loadavg): 1.07 1.02 0.93 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 54967 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223712 134558890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14730 14241 603 41 0 14689 0 vsize: 58920 [startup+559.995 s] Raw data (loadavg): 1.06 1.01 0.93 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 55967 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14730 14241 603 41 0 14689 0 vsize: 58920 [startup+569.994 s] Raw data (loadavg): 1.05 1.01 0.93 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 14264 0 0 0 56967 38 0 0 25 0 1 0 481402018 60334080 14241 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14730 14241 603 41 0 14689 0 vsize: 58920 [startup+579.994 s] Raw data (loadavg): 1.04 1.01 0.93 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 15353 0 0 0 57965 40 0 0 25 0 1 0 481402018 64815104 15330 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15824 15330 603 41 0 15783 0 vsize: 63296 [startup+589.994 s] Raw data (loadavg): 1.03 1.01 0.93 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 16405 0 0 0 58963 43 0 0 25 0 1 0 481402018 69136384 16382 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16879 16382 603 41 0 16838 0 vsize: 67516 [startup+599.994 s] Raw data (loadavg): 1.03 1.01 0.93 2/55 28345 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 17193 0 0 0 59961 45 0 0 25 0 1 0 481402018 72413184 17170 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17679 17170 603 41 0 17638 0 vsize: 70716 [startup+609.994 s] Raw data (loadavg): 1.02 1.01 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 17882 0 0 0 60960 47 0 0 25 0 1 0 481402018 75247616 17859 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18371 17859 603 41 0 18330 0 vsize: 73484 [startup+619.994 s] Raw data (loadavg): 1.02 1.01 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 18741 0 0 0 61957 49 0 0 25 0 1 0 481402018 78753792 18718 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19227 18718 603 41 0 19186 0 vsize: 76908 [startup+629.994 s] Raw data (loadavg): 1.02 1.01 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 19513 0 0 0 62956 51 0 0 25 0 1 0 481402018 81928192 19490 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20002 19490 603 41 0 19961 0 vsize: 80008 [startup+639.995 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 20235 0 0 0 63954 52 0 0 25 0 1 0 481402018 84959232 20212 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20742 20212 603 41 0 20701 0 vsize: 82968 [startup+649.994 s] Raw data (loadavg): 1.01 1.01 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 20811 0 0 0 64954 53 0 0 25 0 1 0 481402018 87310336 20788 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21316 20788 603 41 0 21275 0 vsize: 85264 [startup+659.994 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21337 0 0 0 65953 54 0 0 25 0 1 0 481402018 89600000 21314 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21875 21314 603 41 0 21834 0 vsize: 87500 [startup+669.995 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 66953 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21974 21426 603 41 0 21933 0 vsize: 87896 [startup+679.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 67953 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134561139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21974 21426 603 41 0 21933 0 vsize: 87896 [startup+689.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 68953 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21974 21426 603 41 0 21933 0 vsize: 87896 [startup+699.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 69953 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21974 21426 603 41 0 21933 0 vsize: 87896 [startup+709.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 70953 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21974 21426 603 41 0 21933 0 vsize: 87896 [startup+719.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 71953 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21974 21426 603 41 0 21933 0 vsize: 87896 [startup+729.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 72954 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223632 134560057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21974 21426 603 41 0 21933 0 vsize: 87896 [startup+739.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 73954 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21974 21426 603 41 0 21933 0 vsize: 87896 [startup+749.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 74954 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21974 21426 603 41 0 21933 0 vsize: 87896 [startup+759.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 75954 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21974 21426 603 41 0 21933 0 vsize: 87896 [startup+769.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 76954 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21974 21426 603 41 0 21933 0 vsize: 87896 [startup+779.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21449 0 0 0 77954 55 0 0 25 0 1 0 481402018 90005504 21426 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21974 21426 603 41 0 21933 0 vsize: 87896 [startup+789.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 21930 0 0 0 78953 56 0 0 25 0 1 0 481402018 92028928 21907 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22468 21907 603 41 0 22427 0 vsize: 89872 [startup+799.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 79953 57 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223600 134553549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+809.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 80953 57 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+819.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 81953 57 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223712 134559367 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+829.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 82953 57 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+839.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 83953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+849.997 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 84953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+859.997 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 85953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+869.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 86953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223712 134558658 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+879.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 87953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+889.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 88953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+899.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28347 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 89953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+909.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 90953 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+919.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 91954 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223632 134560335 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+929.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22275 0 0 0 92954 58 0 0 25 0 1 0 481402018 93372416 22252 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22796 22252 603 41 0 22755 0 vsize: 91184 [startup+939.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 22890 0 0 0 93953 60 0 0 25 0 1 0 481402018 95956992 22867 4294967295 134512640 134672761 3221224528 3221223632 134555211 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23427 22867 603 41 0 23386 0 vsize: 93708 [startup+949.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 23772 0 0 0 94951 61 0 0 25 0 1 0 481402018 99606528 23749 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24318 23749 603 41 0 24277 0 vsize: 97272 [startup+959.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 24553 0 0 0 95949 64 0 0 25 0 1 0 481402018 102715392 24530 4294967295 134512640 134672761 3221224528 3221223632 134559916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25077 24530 603 41 0 25036 0 vsize: 100308 [startup+969.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 25299 0 0 0 96948 65 0 0 25 0 1 0 481402018 105852928 25276 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25843 25276 603 41 0 25802 0 vsize: 103372 [startup+979.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 25989 0 0 0 97948 65 0 0 25 0 1 0 481402018 108691456 25966 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26536 25966 603 41 0 26495 0 vsize: 106144 [startup+989.996 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 26583 0 0 0 98947 67 0 0 25 0 1 0 481402018 111140864 26560 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27134 26560 603 41 0 27093 0 vsize: 108536 [startup+999.995 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 27140 0 0 0 99946 68 0 0 25 0 1 0 481402018 113467392 27117 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27702 27117 603 41 0 27661 0 vsize: 110808 [startup+1009.99 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 27572 0 0 0 100945 69 0 0 25 0 1 0 481402018 115367936 27549 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28166 27549 603 41 0 28125 0 vsize: 112664 [startup+1019.99 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 28108 0 0 0 101944 70 0 0 25 0 1 0 481402018 117526528 28085 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28693 28085 603 41 0 28652 0 vsize: 114772 [startup+1030 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 28814 0 0 0 102943 71 0 0 25 0 1 0 481402018 120500224 28791 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29419 28791 603 41 0 29378 0 vsize: 117676 [startup+1040 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29453 0 0 0 103941 73 0 0 25 0 1 0 481402018 123068416 29430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30046 29430 603 41 0 30005 0 vsize: 120184 [startup+1050 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29859 0 0 0 104940 74 0 0 25 0 1 0 481402018 124690432 29836 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30442 29836 603 41 0 30401 0 vsize: 121768 [startup+1059.99 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29859 0 0 0 105940 74 0 0 25 0 1 0 481402018 124690432 29836 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30442 29836 603 41 0 30401 0 vsize: 121768 [startup+1070 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29859 0 0 0 106941 74 0 0 25 0 1 0 481402018 124690432 29836 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30442 29836 603 41 0 30401 0 vsize: 121768 [startup+1080 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29860 0 0 0 107941 74 0 0 25 0 1 0 481402018 124690432 29837 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30442 29837 603 41 0 30401 0 vsize: 121768 [startup+1090 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 108941 74 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30442 29838 603 41 0 30401 0 vsize: 121768 [startup+1100 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 109941 74 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30442 29838 603 41 0 30401 0 vsize: 121768 [startup+1110 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 110941 75 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30442 29838 603 41 0 30401 0 vsize: 121768 [startup+1120 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 111941 75 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30442 29838 603 41 0 30401 0 vsize: 121768 [startup+1130 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 112941 75 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30442 29838 603 41 0 30401 0 vsize: 121768 [startup+1140 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 113941 75 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30442 29838 603 41 0 30401 0 vsize: 121768 [startup+1150 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 114942 75 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30442 29838 603 41 0 30401 0 vsize: 121768 [startup+1160 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 115942 75 0 0 25 0 1 0 481402018 124690432 29838 4294967295 134512640 134672761 3221224528 3221223632 134559991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30442 29838 603 41 0 30401 0 vsize: 121768 [startup+1170 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 116942 75 0 0 25 0 1 0 481402018 124600320 29825 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30420 29825 603 41 0 30379 0 vsize: 121680 [startup+1180 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 117942 75 0 0 25 0 1 0 481402018 124600320 29825 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30420 29825 603 41 0 30379 0 vsize: 121680 [startup+1190 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 118942 75 0 0 25 0 1 0 481402018 124600320 29825 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30420 29825 603 41 0 30379 0 vsize: 121680 [startup+1200 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28349 Raw data (stat): 28341 (minisat+) R 28340 20838 20837 0 -1 0 29861 0 0 0 119942 75 0 0 25 0 1 0 481402018 124600320 29825 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30420 29825 603 41 0 30379 0 vsize: 121680 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.06 s] Raw data (loadavg): 1.00 1.00 0.93 1/55 28349 Raw data (stat): 28341 (minisat+) Z 28340 20838 20837 0 -1 12 29863 0 0 0 119943 80 0 0 25 0 1 0 481402018 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 0 Real time (s): 1200.05 CPU time (s): 1200.24 CPU user time (s): 1199.43 CPU system time (s): 0.809876 CPU usage (%): 100.015 Max. virtual memory (Kb): 121768 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####