Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii32e3.opb |
MD5SUM | fba76bbece6bbaf52b3b51d8d6e74147 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 310 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 660 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 660 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 660 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02584 |
Number of variables | 660 |
Total number of constraints | 5350 |
Number of constraints which are clauses | 5350 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 32 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc30 THE 2005-04-13 20:07:11 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3544 boxname=wulflinc30 idbench=160 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fba76bbece6bbaf52b3b51d8d6e74147 /oldhome/oroussel/tmp/wulflinc30/normalized-ii32e3.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc30/normalized-ii32e3.opb /oldhome/oroussel/tmp/wulflinc30/normalized-ii32e3.opb IDLAUNCH: 3544 /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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 746664 kB Buffers: 37096 kB Cached: 210424 kB SwapCached: 0 kB Active: 79128 kB Inactive: 171184 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 746412 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6928 kB Slab: 32148 kB Committed_AS: 63492 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-13 20:27:13 (client local time) WITH STATUS 10 IN 1200.18 SECONDS stats: 3544 7 1200.18 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 5350 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 | 5350 24606 | 1783 0 0 nan | 0.000 % | c | 100 | 5350 24606 | 1961 100 3833 38.3 | 0.034 % | c ============================================================================== c [1mFound solution: 312[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 1312 maxlim: 348 bits: 10/9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 168 | 14487 57226 | 4829 168 6694 39.8 | 0.034 % | c | 269 | 14487 57226 | 5311 269 11635 43.3 | 0.303 % | c | 419 | 14487 57226 | 5843 419 19768 47.2 | 0.303 % | c | 646 | 14487 57226 | 6427 646 29157 45.1 | 0.303 % | c | 983 | 14487 57226 | 7070 983 45752 46.5 | 0.303 % | c | 1489 | 14487 57226 | 7777 1489 71532 48.0 | 0.303 % | c | 2248 | 14487 57226 | 8554 2248 116467 51.8 | 0.303 % | c | 3387 | 14487 57226 | 9410 3387 202359 59.7 | 0.303 % | c | 5095 | 14487 57226 | 10351 5095 299215 58.7 | 0.303 % | c | 7657 | 14487 57226 | 11386 7657 521108 68.1 | 0.303 % | c | 11501 | 14487 57226 | 12525 11501 685508 59.6 | 0.303 % | c | 17267 | 14487 57226 | 13777 10941 664188 60.7 | 0.303 % | c | 25918 | 14487 57226 | 15155 12627 570987 45.2 | 0.303 % | c | 38893 | 14487 57226 | 16671 8962 828655 92.5 | 0.303 % | c | 58357 | 14487 57226 | 18338 10671 1066714 100.0 | 0.303 % | c | 87550 | 14487 57226 | 20171 10445 1059367 101.4 | 0.303 % | c | 131339 | 14487 57226 | 22189 10983 1007536 91.7 | 0.303 % | c | 197023 | 14487 57226 | 24408 18064 2076677 115.0 | 0.303 % | c | 295549 | 14487 57226 | 26848 25920 2712647 104.7 | 0.303 % | c | 443340 | 14487 57226 | 29533 17523 2514301 143.5 | 0.303 % | #### 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): 1.14 1.02 0.89 2/54 13830 Raw data (stat): 13830 (runsolver) R 13829 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478701894 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.0001 s] Raw data (loadavg): 1.12 1.02 0.89 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 1486 0 0 0 994 4 0 0 25 0 1 0 478701894 7553024 1464 4294967295 134512640 134672761 3221224576 3221223680 134559829 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1844 1464 603 41 0 1803 0 vsize: 7376 [startup+20.0008 s] Raw data (loadavg): 1.10 1.02 0.89 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 1560 0 0 0 1993 5 0 0 25 0 1 0 478701894 7954432 1538 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1942 1538 603 41 0 1901 0 vsize: 7768 [startup+30.0016 s] Raw data (loadavg): 1.08 1.02 0.89 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 2121 0 0 0 2991 7 0 0 25 0 1 0 478701894 10293248 2099 4294967295 134512640 134672761 3221224576 3221223760 134559318 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2513 2099 603 41 0 2472 0 vsize: 10052 [startup+40.0024 s] Raw data (loadavg): 1.07 1.02 0.89 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 2199 0 0 0 3991 7 0 0 25 0 1 0 478701894 10567680 2177 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2580 2177 603 41 0 2539 0 vsize: 10320 [startup+50.0032 s] Raw data (loadavg): 1.06 1.01 0.90 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 2398 0 0 0 4990 9 0 0 25 0 1 0 478701894 11366400 2376 4294967295 134512640 134672761 3221224576 3221223680 134560248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2775 2376 603 41 0 2734 0 vsize: 11100 [startup+60.003 s] Raw data (loadavg): 1.05 1.01 0.90 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 2665 0 0 0 5988 10 0 0 25 0 1 0 478701894 12447744 2643 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3039 2643 603 41 0 2998 0 vsize: 12156 [startup+70.004 s] Raw data (loadavg): 1.04 1.01 0.90 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 2810 0 0 0 6988 11 0 0 25 0 1 0 478701894 13119488 2788 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3203 2788 603 41 0 3162 0 vsize: 12812 [startup+80.0046 s] Raw data (loadavg): 1.04 1.01 0.90 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3008 0 0 0 7986 12 0 0 25 0 1 0 478701894 13918208 2986 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3398 2986 603 41 0 3357 0 vsize: 13592 [startup+90.0053 s] Raw data (loadavg): 1.03 1.01 0.90 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3015 0 0 0 8986 13 0 0 25 0 1 0 478701894 13918208 2993 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3398 2993 603 41 0 3357 0 vsize: 13592 [startup+100.006 s] Raw data (loadavg): 1.02 1.01 0.90 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3376 0 0 0 9985 13 0 0 25 0 1 0 478701894 15405056 3354 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3761 3354 603 41 0 3720 0 vsize: 15044 [startup+110.006 s] Raw data (loadavg): 1.02 1.01 0.90 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3378 0 0 0 10985 14 0 0 25 0 1 0 478701894 15405056 3356 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3761 3356 603 41 0 3720 0 vsize: 15044 [startup+120.007 s] Raw data (loadavg): 1.02 1.01 0.90 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3378 0 0 0 11984 15 0 0 25 0 1 0 478701894 15405056 3356 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3761 3356 603 41 0 3720 0 vsize: 15044 [startup+130.007 s] Raw data (loadavg): 1.01 1.01 0.90 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3753 0 0 0 12983 16 0 0 25 0 1 0 478701894 16883712 3731 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4122 3731 603 41 0 4081 0 vsize: 16488 [startup+140.007 s] Raw data (loadavg): 1.01 1.01 0.90 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 3758 0 0 0 13983 16 0 0 25 0 1 0 478701894 17027072 3736 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4157 3736 603 41 0 4116 0 vsize: 16628 [startup+150.008 s] Raw data (loadavg): 1.01 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4201 0 0 0 14981 18 0 0 25 0 1 0 478701894 18780160 4179 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4585 4179 603 41 0 4544 0 vsize: 18340 [startup+160.008 s] Raw data (loadavg): 1.01 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4275 0 0 0 15981 18 0 0 25 0 1 0 478701894 19046400 4253 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4253 603 41 0 4609 0 vsize: 18600 [startup+170.009 s] Raw data (loadavg): 1.01 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4275 0 0 0 16981 19 0 0 25 0 1 0 478701894 19046400 4253 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4253 603 41 0 4609 0 vsize: 18600 [startup+180.009 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4276 0 0 0 17980 19 0 0 25 0 1 0 478701894 19046400 4254 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4254 603 41 0 4609 0 vsize: 18600 [startup+190.01 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4276 0 0 0 18980 19 0 0 25 0 1 0 478701894 19046400 4254 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4254 603 41 0 4609 0 vsize: 18600 [startup+200.01 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 19980 19 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4255 603 41 0 4609 0 vsize: 18600 [startup+210.01 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 20979 20 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4255 603 41 0 4609 0 vsize: 18600 [startup+220.011 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 21979 20 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223584 134565856 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4255 603 41 0 4609 0 vsize: 18600 [startup+230.01 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 22979 21 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4255 603 41 0 4609 0 vsize: 18600 [startup+240.011 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 23979 21 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4255 603 41 0 4609 0 vsize: 18600 [startup+250.011 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 24978 21 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4255 603 41 0 4609 0 vsize: 18600 [startup+260.012 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 25978 22 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4255 603 41 0 4609 0 vsize: 18600 [startup+270.012 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 26978 22 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4255 603 41 0 4609 0 vsize: 18600 [startup+280.012 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4277 0 0 0 27978 22 0 0 25 0 1 0 478701894 19046400 4255 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4255 603 41 0 4609 0 vsize: 18600 [startup+290.013 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 28978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+300.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 29978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+310.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 30978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+320.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 31978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+330.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 32978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+340.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 33978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+350.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 34978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+360.013 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 35978 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+370.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 36979 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+380.013 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 37979 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+390.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 38979 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+400.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 39979 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+410.013 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4279 0 0 0 40979 23 0 0 25 0 1 0 478701894 19046400 4257 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4650 4257 603 41 0 4609 0 vsize: 18600 [startup+420.013 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4280 0 0 0 41979 23 0 0 25 0 1 0 478701894 19046400 4258 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4650 4258 603 41 0 4609 0 vsize: 18600 [startup+430.013 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4283 0 0 0 42980 23 0 0 25 0 1 0 478701894 19189760 4261 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4685 4261 603 41 0 4644 0 vsize: 18740 [startup+440.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4283 0 0 0 43980 23 0 0 25 0 1 0 478701894 19189760 4261 4294967295 134512640 134672761 3221224576 3221223680 134559985 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4685 4261 603 41 0 4644 0 vsize: 18740 [startup+450.013 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4283 0 0 0 44980 23 0 0 25 0 1 0 478701894 19189760 4261 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4685 4261 603 41 0 4644 0 vsize: 18740 [startup+460.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4284 0 0 0 45979 24 0 0 25 0 1 0 478701894 19189760 4262 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4685 4262 603 41 0 4644 0 vsize: 18740 [startup+470.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4284 0 0 0 46979 24 0 0 25 0 1 0 478701894 19189760 4262 4294967295 134512640 134672761 3221224576 3221223760 134559376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4685 4262 603 41 0 4644 0 vsize: 18740 [startup+480.014 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4285 0 0 0 47979 24 0 0 25 0 1 0 478701894 19189760 4263 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4685 4263 603 41 0 4644 0 vsize: 18740 [startup+490.015 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4285 0 0 0 48979 24 0 0 25 0 1 0 478701894 19189760 4263 4294967295 134512640 134672761 3221224576 3221223760 134559663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4685 4263 603 41 0 4644 0 vsize: 18740 [startup+500.016 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4625 0 0 0 49978 25 0 0 25 0 1 0 478701894 20537344 4603 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5014 4603 603 41 0 4973 0 vsize: 20056 [startup+510.015 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4833 0 0 0 50977 26 0 0 25 0 1 0 478701894 21344256 4811 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5211 4811 603 41 0 5170 0 vsize: 20844 [startup+520.015 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4836 0 0 0 51978 26 0 0 25 0 1 0 478701894 21344256 4814 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5211 4814 603 41 0 5170 0 vsize: 20844 [startup+530.015 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4836 0 0 0 52978 26 0 0 25 0 1 0 478701894 21344256 4814 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5211 4814 603 41 0 5170 0 vsize: 20844 [startup+540.015 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4836 0 0 0 53978 26 0 0 25 0 1 0 478701894 21344256 4814 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5211 4814 603 41 0 5170 0 vsize: 20844 [startup+550.016 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4836 0 0 0 54978 26 0 0 25 0 1 0 478701894 21344256 4814 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5211 4814 603 41 0 5170 0 vsize: 20844 [startup+560.015 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4836 0 0 0 55978 26 0 0 25 0 1 0 478701894 21344256 4814 4294967295 134512640 134672761 3221224576 3221223760 134558918 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5211 4814 603 41 0 5170 0 vsize: 20844 [startup+570.016 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 4836 0 0 0 56978 26 0 0 25 0 1 0 478701894 21344256 4814 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5211 4814 603 41 0 5170 0 vsize: 20844 [startup+580.016 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5319 0 0 0 57977 27 0 0 25 0 1 0 478701894 23355392 5297 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5702 5297 603 41 0 5661 0 vsize: 22808 [startup+590.017 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5517 0 0 0 58977 28 0 0 25 0 1 0 478701894 24162304 5495 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5899 5495 603 41 0 5858 0 vsize: 23596 [startup+600.017 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5517 0 0 0 59977 28 0 0 25 0 1 0 478701894 24162304 5495 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5899 5495 603 41 0 5858 0 vsize: 23596 [startup+610.018 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5517 0 0 0 60977 28 0 0 25 0 1 0 478701894 24162304 5495 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5899 5495 603 41 0 5858 0 vsize: 23596 [startup+620.018 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5517 0 0 0 61977 28 0 0 25 0 1 0 478701894 24162304 5495 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5899 5495 603 41 0 5858 0 vsize: 23596 [startup+630.018 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5517 0 0 0 62977 28 0 0 25 0 1 0 478701894 24162304 5495 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5899 5495 603 41 0 5858 0 vsize: 23596 [startup+640.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5517 0 0 0 63978 28 0 0 25 0 1 0 478701894 24162304 5495 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5899 5495 603 41 0 5858 0 vsize: 23596 [startup+650.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5655 0 0 0 64977 29 0 0 25 0 1 0 478701894 24702976 5633 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6031 5633 603 41 0 5990 0 vsize: 24124 [startup+660.018 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5655 0 0 0 65977 29 0 0 25 0 1 0 478701894 24702976 5633 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6031 5633 603 41 0 5990 0 vsize: 24124 [startup+670.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5655 0 0 0 66978 29 0 0 25 0 1 0 478701894 24702976 5633 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6031 5633 603 41 0 5990 0 vsize: 24124 [startup+680.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5655 0 0 0 67978 29 0 0 25 0 1 0 478701894 24702976 5633 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6031 5633 603 41 0 5990 0 vsize: 24124 [startup+690.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5694 0 0 0 68978 29 0 0 25 0 1 0 478701894 24973312 5672 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6097 5672 603 41 0 6056 0 vsize: 24388 [startup+700.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5694 0 0 0 69978 29 0 0 25 0 1 0 478701894 24973312 5672 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6097 5672 603 41 0 6056 0 vsize: 24388 [startup+710.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5694 0 0 0 70978 29 0 0 25 0 1 0 478701894 24973312 5672 4294967295 134512640 134672761 3221224576 3221223680 134560174 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6097 5672 603 41 0 6056 0 vsize: 24388 [startup+720.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5694 0 0 0 71978 29 0 0 25 0 1 0 478701894 24973312 5672 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6097 5672 603 41 0 6056 0 vsize: 24388 [startup+730.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5694 0 0 0 72978 29 0 0 25 0 1 0 478701894 24973312 5672 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6097 5672 603 41 0 6056 0 vsize: 24388 [startup+740.02 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5695 0 0 0 73979 29 0 0 25 0 1 0 478701894 24973312 5673 4294967295 134512640 134672761 3221224576 3221223760 134559365 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6097 5673 603 41 0 6056 0 vsize: 24388 [startup+750.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5695 0 0 0 74979 29 0 0 25 0 1 0 478701894 24973312 5673 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6097 5673 603 41 0 6056 0 vsize: 24388 [startup+760.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5695 0 0 0 75978 29 0 0 25 0 1 0 478701894 24973312 5673 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6097 5673 603 41 0 6056 0 vsize: 24388 [startup+770.02 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5695 0 0 0 76979 29 0 0 25 0 1 0 478701894 24973312 5673 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6097 5673 603 41 0 6056 0 vsize: 24388 [startup+780.02 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 77979 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6196 5774 603 41 0 6155 0 vsize: 24784 [startup+790.02 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 78979 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6196 5774 603 41 0 6155 0 vsize: 24784 [startup+800.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 79979 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223760 134559417 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6196 5774 603 41 0 6155 0 vsize: 24784 [startup+810.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 80979 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223728 134565212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6196 5774 603 41 0 6155 0 vsize: 24784 [startup+820.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 81979 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6196 5774 603 41 0 6155 0 vsize: 24784 [startup+830.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 82979 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6196 5774 603 41 0 6155 0 vsize: 24784 [startup+840.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 83980 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6196 5774 603 41 0 6155 0 vsize: 24784 [startup+850.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 84980 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6196 5774 603 41 0 6155 0 vsize: 24784 [startup+860.019 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 85980 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6196 5774 603 41 0 6155 0 vsize: 24784 [startup+870.02 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 86980 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6196 5774 603 41 0 6155 0 vsize: 24784 [startup+880.02 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5796 0 0 0 87980 29 0 0 25 0 1 0 478701894 25378816 5774 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6196 5774 603 41 0 6155 0 vsize: 24784 [startup+890.021 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5928 0 0 0 88980 29 0 0 25 0 1 0 478701894 25923584 5906 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6329 5906 603 41 0 6288 0 vsize: 25316 [startup+900.021 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5935 0 0 0 89981 29 0 0 25 0 1 0 478701894 25923584 5913 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6329 5913 603 41 0 6288 0 vsize: 25316 [startup+910.021 s] Raw data (loadavg): 1.07 1.02 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 5936 0 0 0 90981 29 0 0 25 0 1 0 478701894 25923584 5914 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6329 5914 603 41 0 6288 0 vsize: 25316 [startup+920.022 s] Raw data (loadavg): 1.06 1.02 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6118 0 0 0 91980 30 0 0 25 0 1 0 478701894 26726400 6096 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6525 6096 603 41 0 6484 0 vsize: 26100 [startup+930.023 s] Raw data (loadavg): 1.05 1.01 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6200 0 0 0 92980 31 0 0 25 0 1 0 478701894 26992640 6178 4294967295 134512640 134672761 3221224576 3221223712 134565119 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6590 6178 603 41 0 6549 0 vsize: 26360 [startup+940.023 s] Raw data (loadavg): 1.04 1.01 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6201 0 0 0 93980 31 0 0 25 0 1 0 478701894 26992640 6179 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6590 6179 603 41 0 6549 0 vsize: 26360 [startup+950.023 s] Raw data (loadavg): 1.04 1.01 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6201 0 0 0 94980 31 0 0 25 0 1 0 478701894 26992640 6179 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6590 6179 603 41 0 6549 0 vsize: 26360 [startup+960.023 s] Raw data (loadavg): 1.03 1.01 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6348 0 0 0 95980 31 0 0 25 0 1 0 478701894 27668480 6326 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6755 6326 603 41 0 6714 0 vsize: 27020 [startup+970.024 s] Raw data (loadavg): 1.02 1.01 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6492 0 0 0 96980 32 0 0 25 0 1 0 478701894 28205056 6470 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6886 6470 603 41 0 6845 0 vsize: 27544 [startup+980.024 s] Raw data (loadavg): 1.02 1.01 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6492 0 0 0 97980 32 0 0 25 0 1 0 478701894 28205056 6470 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6886 6470 603 41 0 6845 0 vsize: 27544 [startup+990.024 s] Raw data (loadavg): 1.02 1.01 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6492 0 0 0 98980 32 0 0 25 0 1 0 478701894 28205056 6470 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6886 6470 603 41 0 6845 0 vsize: 27544 [startup+1000.02 s] Raw data (loadavg): 1.01 1.01 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6492 0 0 0 99980 32 0 0 25 0 1 0 478701894 28205056 6470 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6886 6470 603 41 0 6845 0 vsize: 27544 [startup+1010.02 s] Raw data (loadavg): 1.01 1.01 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 100980 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1020.02 s] Raw data (loadavg): 1.01 1.01 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 101980 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1030.02 s] Raw data (loadavg): 1.01 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 102980 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1040.03 s] Raw data (loadavg): 1.01 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 103981 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1050.03 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 104981 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1060.02 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 105981 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1070.03 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 106981 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1080.02 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 107981 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1090.02 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 108981 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1100.03 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 109982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223760 134559616 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1110.02 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 110982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1120.02 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 111982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1130.02 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 112982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1140.03 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 113982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1150.03 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 114982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1160.03 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 115982 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1170.03 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 116983 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1180.03 s] Raw data (loadavg): 1.00 1.00 0.91 3/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 117983 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1190.03 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 118983 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 [startup+1200.03 s] Raw data (loadavg): 1.00 1.00 0.91 2/54 13830 Raw data (stat): 13830 (minisat+) R 13829 11931 11930 0 -1 0 6605 0 0 0 119983 32 0 0 25 0 1 0 478701894 28610560 6583 4294967295 134512640 134672761 3221224576 3221223744 134561115 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6985 6583 603 41 0 6944 0 vsize: 27940 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.04 s] Raw data (loadavg): 1.00 1.00 0.91 1/54 13830 Raw data (stat): 13830 (minisat+) Z 13829 11931 11930 0 -1 12 6608 0 0 0 119983 34 0 0 25 0 1 0 478701894 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.04 CPU time (s): 1200.18 CPU user time (s): 1199.84 CPU system time (s): 0.341948 CPU usage (%): 100.012 Max. virtual memory (Kb): 27940 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####