Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl30_35_pb.cnf.cr.opb |
MD5SUM | b1c5adb5438ceaf1c654cfedb79b695e |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
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 | 36 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.06099 |
Number of variables | 2100 |
Total number of constraints | 130 |
Number of constraints which are clauses | 70 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 30 |
Maximum length of a constraint | 35 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc22 THE 2005-04-14 01:38:04 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4148 boxname=wulflinc22 idbench=12 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b1c5adb5438ceaf1c654cfedb79b695e /oldhome/oroussel/tmp/wulflinc22/normalized-chnl30_35_pb.cnf.cr.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc22/normalized-chnl30_35_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc22/normalized-chnl30_35_pb.cnf.cr.opb IDLAUNCH: 4148 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 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: 852816 kB Buffers: 32736 kB Cached: 106004 kB SwapCached: 524 kB Active: 49040 kB Inactive: 93076 kB HighTotal: 131008 kB HighFree: 21336 kB LowTotal: 903652 kB LowFree: 831480 kB SwapTotal: 2097892 kB SwapFree: 2097368 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6924 kB Slab: 34276 kB Committed_AS: 63488 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 01:58:07 (client local time) WITH STATUS 0 IN 1200.19 SECONDS stats: 4148 7 1200.19 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 130 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ...................................................................... c ---[ 59]---> BDD-cost: 67 c ---[ 58]---> BDD-cost: 67 c ---[ 57]---> BDD-cost: 67 c ---[ 56]---> BDD-cost: 67 c ---[ 55]---> BDD-cost: 67 c ---[ 54]---> BDD-cost: 67 c ---[ 53]---> BDD-cost: 67 c ---[ 52]---> BDD-cost: 67 c ---[ 51]---> BDD-cost: 67 c ---[ 50]---> BDD-cost: 67 c ---[ 49]---> BDD-cost: 67 c ---[ 48]---> BDD-cost: 67 c ---[ 47]---> BDD-cost: 67 c ---[ 46]---> BDD-cost: 67 c ---[ 45]---> BDD-cost: 67 c ---[ 44]---> BDD-cost: 67 c ---[ 43]---> BDD-cost: 67 c ---[ 42]---> BDD-cost: 67 c ---[ 41]---> BDD-cost: 67 c ---[ 40]---> BDD-cost: 67 c ---[ 39]---> BDD-cost: 67 c ---[ 38]---> BDD-cost: 67 c ---[ 37]---> BDD-cost: 67 c ---[ 36]---> BDD-cost: 67 c ---[ 35]---> BDD-cost: 67 c ---[ 34]---> BDD-cost: 67 c ---[ 33]---> BDD-cost: 67 c ---[ 32]---> BDD-cost: 67 c ---[ 31]---> BDD-cost: 67 c ---[ 30]---> BDD-cost: 67 c ---[ 29]---> BDD-cost: 67 c ---[ 28]---> BDD-cost: 67 c ---[ 27]---> BDD-cost: 67 c ---[ 26]---> BDD-cost: 67 c ---[ 25]---> BDD-cost: 67 c ---[ 24]---> BDD-cost: 67 c ---[ 23]---> BDD-cost: 67 c ---[ 22]---> BDD-cost: 67 c ---[ 21]---> BDD-cost: 67 c ---[ 20]---> BDD-cost: 67 c ---[ 19]---> BDD-cost: 67 c ---[ 18]---> BDD-cost: 67 c ---[ 17]---> BDD-cost: 67 c ---[ 16]---> BDD-cost: 67 c ---[ 15]---> BDD-cost: 67 c ---[ 14]---> BDD-cost: 67 c ---[ 13]---> BDD-cost: 67 c ---[ 12]---> BDD-cost: 67 c ---[ 11]---> BDD-cost: 67 c ---[ 10]---> BDD-cost: 67 c ---[ 9]---> BDD-cost: 67 c ---[ 8]---> BDD-cost: 67 c ---[ 7]---> BDD-cost: 67 c ---[ 6]---> BDD-cost: 67 c ---[ 5]---> BDD-cost: 67 c ---[ 4]---> BDD-cost: 67 c ---[ 3]---> BDD-cost: 67 c ---[ 2]---> BDD-cost: 67 c ---[ 1]---> BDD-cost: 67 c ---[ 0]---> BDD-cost: 67 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 10030 28020 | 3343 0 0 nan | 0.000 % | c | 105 | 10030 28020 | 3677 105 11655 111.0 | 0.980 % | c | 257 | 10030 28020 | 4045 257 29832 116.1 | 0.980 % | c | 483 | 10030 28020 | 4449 483 70240 145.4 | 0.980 % | c | 822 | 10030 28020 | 4894 822 128798 156.7 | 0.980 % | c | 1332 | 10030 28020 | 5383 1332 212600 159.6 | 0.980 % | c | 2091 | 10030 28020 | 5922 2091 359695 172.0 | 0.980 % | c | 3231 | 10030 28020 | 6514 3231 581665 180.0 | 0.980 % | c | 4941 | 10030 28020 | 7166 4941 1128031 228.3 | 0.980 % | c | 7504 | 10030 28020 | 7882 7504 1889344 251.8 | 0.980 % | c | 11348 | 10030 28020 | 8670 6199 1605192 258.9 | 0.980 % | c | 17117 | 10030 28020 | 9537 6488 1486146 229.1 | 0.980 % | c | 25767 | 10030 28020 | 10491 9195 2320409 252.4 | 0.980 % | c | 38743 | 10030 28020 | 11540 9205 1749321 190.0 | 0.980 % | c | 58205 | 10030 28020 | 12695 7890 2211413 280.3 | 0.980 % | c | 87397 | 10030 28020 | 13964 8204 2185785 266.4 | 0.980 % | c | 131187 | 10030 28020 | 15360 10994 2976111 270.7 | 0.980 % | c | 196872 | 10030 28020 | 16897 18139 5203446 286.9 | 0.980 % | c | 295406 | 10030 28020 | 18586 16345 8504574 520.3 | 0.980 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.84 0.94 0.90 2/54 30876 Raw data (stat): 30876 (runsolver) R 30875 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480688314 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+10.0006 s] Raw data (loadavg): 0.87 0.94 0.90 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 3005 0 0 0 992 6 0 0 25 0 1 0 480688314 13910016 2983 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3396 2983 603 41 0 3355 0 vsize: 13584 [startup+20.0013 s] Raw data (loadavg): 0.89 0.94 0.90 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 3532 0 0 0 1990 8 0 0 25 0 1 0 480688314 16068608 3510 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3923 3510 603 41 0 3882 0 vsize: 15692 [startup+30.0016 s] Raw data (loadavg): 0.90 0.94 0.90 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 3772 0 0 0 2989 9 0 0 25 0 1 0 480688314 17145856 3750 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4186 3750 603 41 0 4145 0 vsize: 16744 [startup+40.0017 s] Raw data (loadavg): 0.92 0.94 0.90 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 4051 0 0 0 3988 10 0 0 25 0 1 0 480688314 18231296 4029 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4451 4029 603 41 0 4410 0 vsize: 17804 [startup+50.0025 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 4337 0 0 0 4987 11 0 0 25 0 1 0 480688314 19447808 4315 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4748 4315 603 41 0 4707 0 vsize: 18992 [startup+60.0028 s] Raw data (loadavg): 0.94 0.95 0.90 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 4338 0 0 0 5987 12 0 0 25 0 1 0 480688314 19447808 4316 4294967295 134512640 134672761 3221224528 3221223712 134558909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4748 4316 603 41 0 4707 0 vsize: 18992 [startup+70.0029 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 4338 0 0 0 6987 12 0 0 25 0 1 0 480688314 19447808 4316 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4748 4316 603 41 0 4707 0 vsize: 18992 [startup+80.0036 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 4400 0 0 0 7987 12 0 0 25 0 1 0 480688314 19718144 4378 4294967295 134512640 134672761 3221224528 3221223632 134559974 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4814 4378 603 41 0 4773 0 vsize: 19256 [startup+90.0039 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5254 0 0 0 8985 14 0 0 25 0 1 0 480688314 23228416 5232 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5671 5232 603 41 0 5630 0 vsize: 22684 [startup+100.005 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5319 0 0 0 9984 15 0 0 25 0 1 0 480688314 23502848 5297 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5738 5297 603 41 0 5697 0 vsize: 22952 [startup+110.006 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5333 0 0 0 10984 15 0 0 25 0 1 0 480688314 23502848 5311 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5738 5311 603 41 0 5697 0 vsize: 22952 [startup+120.006 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5631 0 0 0 11983 17 0 0 25 0 1 0 480688314 24723456 5609 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6036 5609 603 41 0 5995 0 vsize: 24144 [startup+130.007 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5833 0 0 0 12983 17 0 0 25 0 1 0 480688314 25677824 5811 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6269 5811 603 41 0 6228 0 vsize: 25076 [startup+140.008 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5834 0 0 0 13982 18 0 0 25 0 1 0 480688314 25677824 5812 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6269 5812 603 41 0 6228 0 vsize: 25076 [startup+150.008 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5942 0 0 0 14982 18 0 0 25 0 1 0 480688314 26079232 5920 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6367 5920 603 41 0 6326 0 vsize: 25468 [startup+160.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5942 0 0 0 15982 18 0 0 25 0 1 0 480688314 26079232 5920 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6367 5920 603 41 0 6326 0 vsize: 25468 [startup+170.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5942 0 0 0 16982 19 0 0 25 0 1 0 480688314 26079232 5920 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6367 5920 603 41 0 6326 0 vsize: 25468 [startup+180.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5942 0 0 0 17982 19 0 0 25 0 1 0 480688314 26079232 5920 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6367 5920 603 41 0 6326 0 vsize: 25468 [startup+190.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5942 0 0 0 18981 20 0 0 25 0 1 0 480688314 26079232 5920 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6367 5920 603 41 0 6326 0 vsize: 25468 [startup+200.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5942 0 0 0 19981 20 0 0 25 0 1 0 480688314 26079232 5920 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6367 5920 603 41 0 6326 0 vsize: 25468 [startup+210.01 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6407 0 0 0 20980 21 0 0 25 0 1 0 480688314 28172288 6385 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6878 6385 603 41 0 6837 0 vsize: 27512 [startup+220.01 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6408 0 0 0 21980 22 0 0 25 0 1 0 480688314 28172288 6386 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6878 6386 603 41 0 6837 0 vsize: 27512 [startup+230.011 s] Raw data (loadavg): 1.07 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6409 0 0 0 22980 22 0 0 25 0 1 0 480688314 28172288 6387 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6878 6387 603 41 0 6837 0 vsize: 27512 [startup+240.012 s] Raw data (loadavg): 1.06 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6505 0 0 0 23979 22 0 0 25 0 1 0 480688314 28577792 6483 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6977 6483 603 41 0 6936 0 vsize: 27908 [startup+250.012 s] Raw data (loadavg): 1.05 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6505 0 0 0 24979 22 0 0 25 0 1 0 480688314 28577792 6483 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6977 6483 603 41 0 6936 0 vsize: 27908 [startup+260.013 s] Raw data (loadavg): 1.04 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6512 0 0 0 25979 22 0 0 25 0 1 0 480688314 28577792 6490 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6977 6490 603 41 0 6936 0 vsize: 27908 [startup+270.012 s] Raw data (loadavg): 1.04 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6809 0 0 0 26978 23 0 0 25 0 1 0 480688314 29794304 6787 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7274 6787 603 41 0 7233 0 vsize: 29096 [startup+280.013 s] Raw data (loadavg): 1.03 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7145 0 0 0 27977 25 0 0 25 0 1 0 480688314 31145984 7123 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7604 7123 603 41 0 7563 0 vsize: 30416 [startup+290.014 s] Raw data (loadavg): 1.03 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7154 0 0 0 28977 25 0 0 25 0 1 0 480688314 31293440 7132 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7640 7132 603 41 0 7599 0 vsize: 30560 [startup+300.013 s] Raw data (loadavg): 1.02 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7154 0 0 0 29977 26 0 0 25 0 1 0 480688314 31293440 7132 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7640 7132 603 41 0 7599 0 vsize: 30560 [startup+310.014 s] Raw data (loadavg): 1.02 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7154 0 0 0 30977 26 0 0 25 0 1 0 480688314 31293440 7132 4294967295 134512640 134672761 3221224528 3221223712 134559538 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7640 7132 603 41 0 7599 0 vsize: 30560 [startup+320.014 s] Raw data (loadavg): 1.01 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7157 0 0 0 31977 26 0 0 25 0 1 0 480688314 31293440 7135 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7640 7135 603 41 0 7599 0 vsize: 30560 [startup+330.015 s] Raw data (loadavg): 1.01 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7158 0 0 0 32976 26 0 0 25 0 1 0 480688314 31293440 7136 4294967295 134512640 134672761 3221224528 3221223632 134559853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7640 7136 603 41 0 7599 0 vsize: 30560 [startup+340.015 s] Raw data (loadavg): 1.01 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7985 0 0 0 33974 29 0 0 25 0 1 0 480688314 34660352 7963 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8462 7963 603 41 0 8421 0 vsize: 33848 [startup+350.015 s] Raw data (loadavg): 1.01 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8030 0 0 0 34973 29 0 0 25 0 1 0 480688314 34795520 8008 4294967295 134512640 134672761 3221224528 3221223600 134553549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8495 8008 603 41 0 8454 0 vsize: 33980 [startup+360.016 s] Raw data (loadavg): 1.01 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8030 0 0 0 35973 30 0 0 25 0 1 0 480688314 34795520 8008 4294967295 134512640 134672761 3221224528 3221223624 1075347186 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8495 8008 603 41 0 8454 0 vsize: 33980 [startup+370.015 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8030 0 0 0 36973 30 0 0 25 0 1 0 480688314 34795520 8008 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8495 8008 603 41 0 8454 0 vsize: 33980 [startup+380.016 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8256 0 0 0 37973 31 0 0 25 0 1 0 480688314 35741696 8234 4294967295 134512640 134672761 3221224528 3221223632 134560048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8726 8234 603 41 0 8685 0 vsize: 34904 [startup+390.017 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8256 0 0 0 38972 31 0 0 25 0 1 0 480688314 35741696 8234 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8726 8234 603 41 0 8685 0 vsize: 34904 [startup+400.017 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8256 0 0 0 39973 31 0 0 25 0 1 0 480688314 35741696 8234 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8726 8234 603 41 0 8685 0 vsize: 34904 [startup+410.018 s] Raw data (loadavg): 1.08 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8298 0 0 0 40972 31 0 0 25 0 1 0 480688314 35876864 8276 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8759 8276 603 41 0 8718 0 vsize: 35036 [startup+420.018 s] Raw data (loadavg): 1.07 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8615 0 0 0 41971 32 0 0 25 0 1 0 480688314 37302272 8593 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9107 8593 603 41 0 9066 0 vsize: 36428 [startup+430.019 s] Raw data (loadavg): 1.06 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8615 0 0 0 42971 33 0 0 25 0 1 0 480688314 37302272 8593 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9107 8593 603 41 0 9066 0 vsize: 36428 [startup+440.019 s] Raw data (loadavg): 1.05 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8615 0 0 0 43971 33 0 0 25 0 1 0 480688314 37302272 8593 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9107 8593 603 41 0 9066 0 vsize: 36428 [startup+450.019 s] Raw data (loadavg): 1.04 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8615 0 0 0 44970 33 0 0 25 0 1 0 480688314 37302272 8593 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9107 8593 603 41 0 9066 0 vsize: 36428 [startup+460.019 s] Raw data (loadavg): 1.03 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9017 0 0 0 45970 34 0 0 25 0 1 0 480688314 38916096 8995 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9501 8995 603 41 0 9460 0 vsize: 38004 [startup+470.02 s] Raw data (loadavg): 1.03 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9056 0 0 0 46969 35 0 0 25 0 1 0 480688314 39051264 9034 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9534 9034 603 41 0 9493 0 vsize: 38136 [startup+480.02 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9056 0 0 0 47969 35 0 0 25 0 1 0 480688314 39051264 9034 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9534 9034 603 41 0 9493 0 vsize: 38136 [startup+490.021 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9162 0 0 0 48969 36 0 0 25 0 1 0 480688314 39452672 9140 4294967295 134512640 134672761 3221224528 3221223632 134560158 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9632 9140 603 41 0 9591 0 vsize: 38528 [startup+500.021 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9328 0 0 0 49968 36 0 0 25 0 1 0 480688314 40132608 9306 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9798 9306 603 41 0 9757 0 vsize: 39192 [startup+510.021 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9329 0 0 0 50968 37 0 0 25 0 1 0 480688314 40132608 9307 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9798 9307 603 41 0 9757 0 vsize: 39192 [startup+520.021 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9330 0 0 0 51967 37 0 0 25 0 1 0 480688314 40132608 9308 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9798 9308 603 41 0 9757 0 vsize: 39192 [startup+530.022 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9330 0 0 0 52967 37 0 0 25 0 1 0 480688314 40132608 9308 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9798 9308 603 41 0 9757 0 vsize: 39192 [startup+540.023 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9346 0 0 0 53967 37 0 0 25 0 1 0 480688314 40284160 9324 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9835 9324 603 41 0 9794 0 vsize: 39340 [startup+550.022 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9358 0 0 0 54967 38 0 0 25 0 1 0 480688314 40284160 9336 4294967295 134512640 134672761 3221224528 3221223712 134558875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9835 9336 603 41 0 9794 0 vsize: 39340 [startup+560.022 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9358 0 0 0 55967 38 0 0 25 0 1 0 480688314 40284160 9336 4294967295 134512640 134672761 3221224528 3221223632 134560212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9835 9336 603 41 0 9794 0 vsize: 39340 [startup+570.023 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9358 0 0 0 56967 38 0 0 25 0 1 0 480688314 40284160 9336 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9835 9336 603 41 0 9794 0 vsize: 39340 [startup+580.023 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9358 0 0 0 57967 39 0 0 25 0 1 0 480688314 40284160 9336 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9835 9336 603 41 0 9794 0 vsize: 39340 [startup+590.024 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9426 0 0 0 58966 39 0 0 25 0 1 0 480688314 40689664 9404 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9934 9404 603 41 0 9893 0 vsize: 39736 [startup+600.025 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 10229 0 0 0 59964 41 0 0 25 0 1 0 480688314 43929600 10207 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10725 10207 603 41 0 10684 0 vsize: 42900 [startup+610.026 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 10229 0 0 0 60964 41 0 0 25 0 1 0 480688314 43929600 10207 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10725 10207 603 41 0 10684 0 vsize: 42900 [startup+620.025 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 11274 0 0 0 61962 44 0 0 25 0 1 0 480688314 48168960 11252 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11760 11252 603 41 0 11719 0 vsize: 47040 [startup+630.026 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12108 0 0 0 62960 46 0 0 25 0 1 0 480688314 51683328 12086 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12618 12086 603 41 0 12577 0 vsize: 50472 [startup+640.026 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12109 0 0 0 63960 46 0 0 25 0 1 0 480688314 51683328 12087 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12618 12087 603 41 0 12577 0 vsize: 50472 [startup+650.027 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12109 0 0 0 64960 46 0 0 25 0 1 0 480688314 51683328 12087 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12618 12087 603 41 0 12577 0 vsize: 50472 [startup+660.027 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12109 0 0 0 65960 46 0 0 25 0 1 0 480688314 51683328 12087 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12618 12087 603 41 0 12577 0 vsize: 50472 [startup+670.027 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12109 0 0 0 66960 47 0 0 25 0 1 0 480688314 51683328 12087 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12618 12087 603 41 0 12577 0 vsize: 50472 [startup+680.029 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 67958 48 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13045 12526 603 41 0 13004 0 vsize: 52180 [startup+690.029 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 68958 48 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223712 134558761 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13045 12526 603 41 0 13004 0 vsize: 52180 [startup+700.031 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 69958 49 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223696 134561009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13045 12526 603 41 0 13004 0 vsize: 52180 [startup+710.032 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 70959 49 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13045 12526 603 41 0 13004 0 vsize: 52180 [startup+720.031 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 71959 49 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223712 134559498 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13045 12526 603 41 0 13004 0 vsize: 52180 [startup+730.033 s] Raw data (loadavg): 1.00 1.00 0.92 3/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 72959 49 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13045 12526 603 41 0 13004 0 vsize: 52180 [startup+740.034 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 73959 49 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13045 12526 603 41 0 13004 0 vsize: 52180 [startup+750.033 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 74959 49 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13045 12526 603 41 0 13004 0 vsize: 52180 [startup+760.035 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12549 0 0 0 75959 49 0 0 25 0 1 0 480688314 53432320 12527 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13045 12527 603 41 0 13004 0 vsize: 52180 [startup+770.035 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 13157 0 0 0 76958 51 0 0 25 0 1 0 480688314 56000512 13135 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13672 13135 603 41 0 13631 0 vsize: 54688 [startup+780.035 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 13598 0 0 0 77957 52 0 0 25 0 1 0 480688314 57761792 13576 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14102 13576 603 41 0 14061 0 vsize: 56408 [startup+790.035 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 13598 0 0 0 78957 52 0 0 25 0 1 0 480688314 57761792 13576 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14102 13576 603 41 0 14061 0 vsize: 56408 [startup+800.035 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 13598 0 0 0 79957 52 0 0 25 0 1 0 480688314 57761792 13576 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14102 13576 603 41 0 14061 0 vsize: 56408 [startup+810.035 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 13599 0 0 0 80957 52 0 0 25 0 1 0 480688314 57761792 13577 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14102 13577 603 41 0 14061 0 vsize: 56408 [startup+820.035 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 13806 0 0 0 81958 52 0 0 25 0 1 0 480688314 58572800 13784 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14300 13784 603 41 0 14259 0 vsize: 57200 [startup+830.036 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 82954 56 0 0 25 0 1 0 480688314 62627840 14760 4294967295 134512640 134672761 3221224528 3221223632 134554656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15290 14760 603 41 0 15249 0 vsize: 61160 [startup+840.036 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 83954 56 0 0 25 0 1 0 480688314 62627840 14760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15290 14760 603 41 0 15249 0 vsize: 61160 [startup+850.036 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 84954 56 0 0 25 0 1 0 480688314 62627840 14760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15290 14760 603 41 0 15249 0 vsize: 61160 [startup+860.037 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 85954 56 0 0 25 0 1 0 480688314 62627840 14760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15290 14760 603 41 0 15249 0 vsize: 61160 [startup+870.037 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 86955 56 0 0 25 0 1 0 480688314 62599168 14760 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15283 14760 603 41 0 15242 0 vsize: 61132 [startup+880.038 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 87955 56 0 0 25 0 1 0 480688314 62599168 14760 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15283 14760 603 41 0 15242 0 vsize: 61132 [startup+890.038 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 88955 56 0 0 25 0 1 0 480688314 62599168 14760 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15283 14760 603 41 0 15242 0 vsize: 61132 [startup+900.037 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 89955 56 0 0 25 0 1 0 480688314 62599168 14760 4294967295 134512640 134672761 3221224528 3221223664 134565070 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15283 14760 603 41 0 15242 0 vsize: 61132 [startup+910.038 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 90955 56 0 0 25 0 1 0 480688314 62595072 14760 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15282 14760 603 41 0 15241 0 vsize: 61128 [startup+920.037 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 91955 56 0 0 25 0 1 0 480688314 62595072 14760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15282 14760 603 41 0 15241 0 vsize: 61128 [startup+930.038 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 92955 56 0 0 25 0 1 0 480688314 62595072 14760 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15282 14760 603 41 0 15241 0 vsize: 61128 [startup+940.039 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 93955 57 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+950.039 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 94955 57 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+960.039 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 95955 57 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+970.039 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 96955 57 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+980.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 97955 57 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223632 134560048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+990.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 98955 58 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+1000.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 99955 58 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+1010.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 100955 58 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+1020.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 101954 58 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+1030.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 102954 59 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+1040.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 103954 59 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+1050.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 104954 59 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+1060.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 105954 60 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+1070.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 106954 60 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+1080.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 107953 60 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+1090.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 108954 60 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+1100.04 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 109954 60 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15259 14749 603 41 0 15218 0 vsize: 61036 [startup+1110.04 s] Raw data (loadavg): 1.08 1.01 0.93 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 110953 61 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15257 14747 603 41 0 15216 0 vsize: 61028 [startup+1120.04 s] Raw data (loadavg): 1.07 1.01 0.93 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 111953 61 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15257 14747 603 41 0 15216 0 vsize: 61028 [startup+1130.05 s] Raw data (loadavg): 1.06 1.01 0.93 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 112953 61 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223712 134559356 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15257 14747 603 41 0 15216 0 vsize: 61028 [startup+1140.05 s] Raw data (loadavg): 1.05 1.01 0.93 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 113953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15257 14747 603 41 0 15216 0 vsize: 61028 [startup+1150.05 s] Raw data (loadavg): 1.04 1.01 0.93 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 114953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15257 14747 603 41 0 15216 0 vsize: 61028 [startup+1160.05 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 115953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15257 14747 603 41 0 15216 0 vsize: 61028 [startup+1170.05 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 116953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15257 14747 603 41 0 15216 0 vsize: 61028 [startup+1180.05 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 117953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15257 14747 603 41 0 15216 0 vsize: 61028 [startup+1190.05 s] Raw data (loadavg): 1.02 1.00 0.93 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 118953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15257 14747 603 41 0 15216 0 vsize: 61028 [startup+1200.05 s] Raw data (loadavg): 1.02 1.00 0.93 2/54 30876 Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 119953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15257 14747 603 41 0 15216 0 vsize: 61028 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.08 s] Raw data (loadavg): 1.02 1.00 0.93 1/54 30876 Raw data (stat): 30876 (minisat+) Z 30875 26298 26297 0 -1 12 14786 0 0 0 119953 65 0 0 25 0 1 0 480688314 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.08 CPU time (s): 1200.19 CPU user time (s): 1199.54 CPU system time (s): 0.6549 CPU usage (%): 100.01 Max. virtual memory (Kb): 61160 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####