Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga35_35_sat_pb.cnf.cr.opb |
MD5SUM | 022f43a9cfc62e9c9c77f51c14f8e5bf |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 36 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.88771 |
Number of variables | 1838 |
Total number of constraints | 1330 |
Number of constraints which are clauses | 1260 |
Number of constraints which are cardinality constraints (but not clauses) | 70 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 17 |
Maximum length of a constraint | 35 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc29 THE 2005-04-13 23:40:44 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3811 boxname=wulflinc29 idbench=51 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 022f43a9cfc62e9c9c77f51c14f8e5bf /oldhome/oroussel/tmp/wulflinc29/normalized-fpga35_35_sat_pb.cnf.cr.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc29/normalized-fpga35_35_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc29/normalized-fpga35_35_sat_pb.cnf.cr.opb IDLAUNCH: 3811 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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.020 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: 833412 kB Buffers: 35872 kB Cached: 128132 kB SwapCached: 12 kB Active: 53156 kB Inactive: 113716 kB HighTotal: 131008 kB HighFree: 448 kB LowTotal: 903652 kB LowFree: 832964 kB SwapTotal: 2097892 kB SwapFree: 2097880 kB Dirty: 36 kB Writeback: 0 kB Mapped: 6928 kB Slab: 28948 kB Committed_AS: 63492 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-13 23:52:47 (client local time) WITH STATUS 30 IN 723.007 SECONDS stats: 3811 7 723.007 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 1330 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ c ---[ 69]---> BDD-cost: 67 c ---[ 68]---> BDD-cost: 67 c ---[ 67]---> BDD-cost: 67 c ---[ 66]---> BDD-cost: 67 c ---[ 65]---> BDD-cost: 67 c ---[ 64]---> BDD-cost: 67 c ---[ 63]---> BDD-cost: 67 c ---[ 62]---> BDD-cost: 67 c ---[ 61]---> BDD-cost: 67 c ---[ 60]---> BDD-cost: 67 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: 31 c ---[ 33]---> BDD-cost: 31 c ---[ 32]---> BDD-cost: 31 c ---[ 31]---> BDD-cost: 31 c ---[ 30]---> BDD-cost: 31 c ---[ 29]---> BDD-cost: 31 c ---[ 28]---> BDD-cost: 31 c ---[ 27]---> BDD-cost: 31 c ---[ 26]---> BDD-cost: 31 c ---[ 25]---> BDD-cost: 31 c ---[ 24]---> BDD-cost: 31 c ---[ 23]---> BDD-cost: 31 c ---[ 22]---> BDD-cost: 31 c ---[ 21]---> BDD-cost: 31 c ---[ 20]---> BDD-cost: 31 c ---[ 19]---> BDD-cost: 31 c ---[ 18]---> BDD-cost: 31 c ---[ 17]---> BDD-cost: 33 c ---[ 16]---> BDD-cost: 33 c ---[ 15]---> BDD-cost: 33 c ---[ 14]---> BDD-cost: 33 c ---[ 13]---> BDD-cost: 33 c ---[ 12]---> BDD-cost: 33 c ---[ 11]---> BDD-cost: 33 c ---[ 10]---> BDD-cost: 33 c ---[ 9]---> BDD-cost: 33 c ---[ 8]---> BDD-cost: 33 c ---[ 7]---> BDD-cost: 33 c ---[ 6]---> BDD-cost: 33 c ---[ 5]---> BDD-cost: 33 c ---[ 4]---> BDD-cost: 33 c ---[ 3]---> BDD-cost: 33 c ---[ 2]---> BDD-cost: 33 c ---[ 1]---> BDD-cost: 33 c ---[ 0]---> BDD-cost: 33 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 9820 46189 | 2945 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/5234 c -- var.elim.: 2000/5234 c -- var.elim.: 3000/5234 c -- var.elim.: 4000/5234 c -- var.elim.: 5000/5234 c -- var.elim.: 5234/5234 c -- var.elim.: 1000/1725 c -- var.elim.: 1725/1725 c -- subsuming c -- var.elim.: 1000/1453 c -- var.elim.: 1453/1453 c -- var.elim.: 1000/1596 c -- var.elim.: 1596/1596 c -- subsuming c -- var.elim.: 611/611 c -- var.elim.: 1000/1287 c -- var.elim.: 1287/1287 c -- subsuming c -- var.elim.: 1000/1199 c -- var.elim.: 1199/1199 c -- var.elim.: 55/55 c | 0 | 9299 47689 | -- 0 -- -- | -- | -521/1710 c | 0 | 9299 47689 | 3719 0 0 nan | 0.000 % | c | 100 | 9299 47689 | 4091 100 24785 247.8 | 1.422 % | c | 253 | 9299 47689 | 4500 253 64605 255.4 | 1.422 % | c | 479 | 9299 47689 | 4950 479 104371 217.9 | 1.422 % | c | 816 | 9299 47689 | 5445 816 160400 196.6 | 1.422 % | c | 1324 | 9299 47689 | 5990 1324 286698 216.5 | 1.422 % | c | 2083 | 9299 47689 | 6589 2083 491113 235.8 | 1.422 % | c | 3222 | 9299 47689 | 7248 3222 765397 237.6 | 1.422 % | c | 4930 | 9299 47689 | 7973 4930 1161371 235.6 | 1.422 % | c | 7493 | 9299 47689 | 8770 7493 1837865 245.3 | 1.422 % | c | 11339 | 9299 47689 | 9647 11339 2590641 228.5 | 1.422 % | c | 17106 | 9299 47689 | 10612 9002 2998815 333.1 | 1.422 % | c | 25756 | 9299 47689 | 11673 13058 4814817 368.7 | 1.422 % | c | 38730 | 9299 47689 | 12841 12028 3455866 287.3 | 1.422 % | c | 58195 | 9299 47689 | 14125 11216 2996384 267.2 | 1.422 % | c | 87387 | 9299 47689 | 15537 11895 4140890 348.1 | 1.422 % | c | 131176 | 9299 47689 | 17091 15960 3845369 240.9 | 1.422 % | c ============================================================================== c (current CPU-time: 722.662 s) c ============================================================================== c [1mSATISFIABLE: No goal function specified.[0m s SATISFIABLE v c _______________________________________________________________________________ c c restarts : 17 c conflicts : 191962 (266 /sec) c decisions : 250364 (346 /sec) c propagations : 25313659 (35027 /sec) c inspects : 549709482 (760643 /sec) c CPU time : 722.69 s c _______________________________________________________________________________ #### 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.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (runsolver) R 31807 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479983228 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+9.99975 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 3607 0 0 0 989 8 0 0 25 0 1 0 479983228 16502784 3566 4294967295 134512640 134672761 3221224528 3221223568 134603565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4029 3567 603 41 0 3988 0 vsize: 16116 [startup+20.0002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 4294 0 0 0 1988 10 0 0 25 0 1 0 479983228 19267584 4253 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4704 4253 603 41 0 4663 0 vsize: 18816 [startup+30.0003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 5307 0 0 0 2985 13 0 0 25 0 1 0 479983228 23355392 5266 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5702 5266 603 41 0 5661 0 vsize: 22808 [startup+40.0011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6052 0 0 0 3983 15 0 0 25 0 1 0 479983228 26521600 6011 4294967295 134512640 134672761 3221224528 3221223624 134616183 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6475 6011 603 41 0 6434 0 vsize: 25900 [startup+50.0019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6354 0 0 0 4982 16 0 0 25 0 1 0 479983228 27635712 6313 4294967295 134512640 134672761 3221224528 3221223688 134614557 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6747 6313 603 41 0 6706 0 vsize: 26988 [startup+60.0017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6355 0 0 0 5982 16 0 0 25 0 1 0 479983228 27635712 6314 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6747 6314 603 41 0 6706 0 vsize: 26988 [startup+70.0024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6355 0 0 0 6983 16 0 0 25 0 1 0 479983228 27635712 6314 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6747 6314 603 41 0 6706 0 vsize: 26988 [startup+80.0019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6355 0 0 0 7983 16 0 0 25 0 1 0 479983228 27635712 6314 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6747 6314 603 41 0 6706 0 vsize: 26988 [startup+90.0017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6355 0 0 0 8983 16 0 0 25 0 1 0 479983228 27635712 6314 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6747 6314 603 41 0 6706 0 vsize: 26988 [startup+100.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6356 0 0 0 9983 16 0 0 25 0 1 0 479983228 27635712 6315 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6747 6315 603 41 0 6706 0 vsize: 26988 [startup+110.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6514 0 0 0 10983 16 0 0 25 0 1 0 479983228 28291072 6473 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6907 6473 603 41 0 6866 0 vsize: 27628 [startup+120.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6921 0 0 0 11983 17 0 0 25 0 1 0 479983228 29999104 6880 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7324 6880 603 41 0 7283 0 vsize: 29296 [startup+130.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6921 0 0 0 12983 17 0 0 25 0 1 0 479983228 29999104 6880 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7324 6880 603 41 0 7283 0 vsize: 29296 [startup+140.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6921 0 0 0 13983 17 0 0 25 0 1 0 479983228 29999104 6880 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7324 6880 603 41 0 7283 0 vsize: 29296 [startup+150.002 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6921 0 0 0 14983 17 0 0 25 0 1 0 479983228 29999104 6880 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7324 6880 603 41 0 7283 0 vsize: 29296 [startup+160.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6921 0 0 0 15983 17 0 0 25 0 1 0 479983228 29999104 6880 4294967295 134512640 134672761 3221224528 3221223728 134610686 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7324 6880 603 41 0 7283 0 vsize: 29296 [startup+170.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6939 0 0 0 16984 17 0 0 25 0 1 0 479983228 30142464 6898 4294967295 134512640 134672761 3221224528 3221223568 134612619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7359 6898 603 41 0 7318 0 vsize: 29436 [startup+180.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6939 0 0 0 17984 17 0 0 25 0 1 0 479983228 30142464 6898 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7359 6898 603 41 0 7318 0 vsize: 29436 [startup+190.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 6939 0 0 0 18984 17 0 0 25 0 1 0 479983228 30142464 6898 4294967295 134512640 134672761 3221224528 3221223712 134615689 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7359 6898 603 41 0 7318 0 vsize: 29436 [startup+200.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 7164 0 0 0 19983 18 0 0 25 0 1 0 479983228 31064064 7123 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7584 7123 603 41 0 7543 0 vsize: 30336 [startup+210.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 7164 0 0 0 20984 18 0 0 25 0 1 0 479983228 31064064 7123 4294967295 134512640 134672761 3221224528 3221223664 134614724 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7584 7123 603 41 0 7543 0 vsize: 30336 [startup+220.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 7164 0 0 0 21984 18 0 0 25 0 1 0 479983228 31064064 7123 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7584 7123 603 41 0 7543 0 vsize: 30336 [startup+230.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 7594 0 0 0 22983 19 0 0 25 0 1 0 479983228 32808960 7553 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8010 7553 603 41 0 7969 0 vsize: 32040 [startup+240.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 7848 0 0 0 23982 20 0 0 25 0 1 0 479983228 33890304 7806 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8274 7806 603 41 0 8233 0 vsize: 33096 [startup+250.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 7848 0 0 0 24982 20 0 0 25 0 1 0 479983228 33890304 7806 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8274 7806 603 41 0 8233 0 vsize: 33096 [startup+260.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 7848 0 0 0 25982 20 0 0 25 0 1 0 479983228 33890304 7806 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8274 7806 603 41 0 8233 0 vsize: 33096 [startup+270.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8144 0 0 0 26982 20 0 0 25 0 1 0 479983228 35098624 8101 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8569 8101 603 41 0 8528 0 vsize: 34276 [startup+280.005 s] Raw data (loadavg): 1.07 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8144 0 0 0 27982 20 0 0 25 0 1 0 479983228 35098624 8101 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8569 8101 603 41 0 8528 0 vsize: 34276 [startup+290.005 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8144 0 0 0 28982 20 0 0 25 0 1 0 479983228 35098624 8101 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8569 8101 603 41 0 8528 0 vsize: 34276 [startup+300.005 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8490 0 0 0 29982 21 0 0 25 0 1 0 479983228 36552704 8447 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8924 8447 603 41 0 8883 0 vsize: 35696 [startup+310.005 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8491 0 0 0 30982 21 0 0 25 0 1 0 479983228 36552704 8448 4294967295 134512640 134672761 3221224528 3221223712 134615926 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8924 8448 603 41 0 8883 0 vsize: 35696 [startup+320.006 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8493 0 0 0 31982 21 0 0 25 0 1 0 479983228 36552704 8450 4294967295 134512640 134672761 3221224528 3221223712 134615739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8924 8450 603 41 0 8883 0 vsize: 35696 [startup+330.006 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8493 0 0 0 32983 21 0 0 25 0 1 0 479983228 36552704 8450 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8924 8450 603 41 0 8883 0 vsize: 35696 [startup+340.006 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8494 0 0 0 33983 21 0 0 25 0 1 0 479983228 36548608 8450 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8450 603 41 0 8882 0 vsize: 35692 [startup+350.005 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8494 0 0 0 34983 21 0 0 25 0 1 0 479983228 36548608 8450 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8450 603 41 0 8882 0 vsize: 35692 [startup+360.005 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8494 0 0 0 35983 21 0 0 25 0 1 0 479983228 36548608 8450 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8450 603 41 0 8882 0 vsize: 35692 [startup+370.006 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8494 0 0 0 36983 21 0 0 25 0 1 0 479983228 36548608 8450 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8450 603 41 0 8882 0 vsize: 35692 [startup+380.005 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8494 0 0 0 37983 21 0 0 25 0 1 0 479983228 36548608 8450 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8450 603 41 0 8882 0 vsize: 35692 [startup+390.005 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8494 0 0 0 38984 21 0 0 25 0 1 0 479983228 36548608 8450 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8450 603 41 0 8882 0 vsize: 35692 [startup+400.005 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8494 0 0 0 39984 21 0 0 25 0 1 0 479983228 36548608 8450 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8450 603 41 0 8882 0 vsize: 35692 [startup+410.007 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8494 0 0 0 40984 21 0 0 25 0 1 0 479983228 36548608 8450 4294967295 134512640 134672761 3221224528 3221223584 134644260 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8450 603 41 0 8882 0 vsize: 35692 [startup+420.007 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8494 0 0 0 41984 21 0 0 25 0 1 0 479983228 36548608 8450 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8450 603 41 0 8882 0 vsize: 35692 [startup+430.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8494 0 0 0 42984 21 0 0 25 0 1 0 479983228 36548608 8450 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8450 603 41 0 8882 0 vsize: 35692 [startup+440.008 s] Raw data (loadavg): 1.00 0.99 0.91 3/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8494 0 0 0 43985 21 0 0 25 0 1 0 479983228 36548608 8450 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8450 603 41 0 8882 0 vsize: 35692 [startup+450.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8495 0 0 0 44985 21 0 0 25 0 1 0 479983228 36548608 8451 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8451 603 41 0 8882 0 vsize: 35692 [startup+460.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8495 0 0 0 45985 21 0 0 25 0 1 0 479983228 36548608 8451 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8451 603 41 0 8882 0 vsize: 35692 [startup+470.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8495 0 0 0 46985 21 0 0 25 0 1 0 479983228 36548608 8451 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8923 8451 603 41 0 8882 0 vsize: 35692 [startup+480.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8925 0 0 0 47985 22 0 0 25 0 1 0 479983228 38309888 8880 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9353 8880 603 41 0 9312 0 vsize: 37412 [startup+490.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 8925 0 0 0 48985 22 0 0 25 0 1 0 479983228 38309888 8880 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9353 8880 603 41 0 9312 0 vsize: 37412 [startup+500.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 9627 0 0 0 49984 23 0 0 25 0 1 0 479983228 41213952 9582 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10062 9582 603 41 0 10021 0 vsize: 40248 [startup+510.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 10303 0 0 0 50982 25 0 0 25 0 1 0 479983228 44007424 10258 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10744 10258 603 41 0 10703 0 vsize: 42976 [startup+520.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 10975 0 0 0 51981 26 0 0 25 0 1 0 479983228 46792704 10930 4294967295 134512640 134672761 3221224528 3221223584 134644275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11424 10930 603 41 0 11383 0 vsize: 45696 [startup+530.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 10976 0 0 0 52981 26 0 0 25 0 1 0 479983228 46727168 10931 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11408 10931 603 41 0 11367 0 vsize: 45632 [startup+540.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 10979 0 0 0 53981 26 0 0 25 0 1 0 479983228 46727168 10934 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11408 10934 603 41 0 11367 0 vsize: 45632 [startup+550.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 10990 0 0 0 54982 26 0 0 25 0 1 0 479983228 46923776 10945 4294967295 134512640 134672761 3221224528 3221223568 134614205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11456 10945 603 41 0 11415 0 vsize: 45824 [startup+560.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11246 0 0 0 55981 27 0 0 25 0 1 0 479983228 47853568 11201 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11683 11201 603 41 0 11642 0 vsize: 46732 [startup+570.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11464 0 0 0 56981 27 0 0 25 0 1 0 479983228 48803840 11419 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11915 11419 603 41 0 11874 0 vsize: 47660 [startup+580.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11464 0 0 0 57982 27 0 0 25 0 1 0 479983228 48803840 11419 4294967295 134512640 134672761 3221224528 3221223712 134615739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11915 11419 603 41 0 11874 0 vsize: 47660 [startup+590.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11465 0 0 0 58982 27 0 0 25 0 1 0 479983228 48803840 11420 4294967295 134512640 134672761 3221224528 3221223712 134615643 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11915 11420 603 41 0 11874 0 vsize: 47660 [startup+600.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11467 0 0 0 59982 27 0 0 25 0 1 0 479983228 48803840 11422 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11915 11422 603 41 0 11874 0 vsize: 47660 [startup+610.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11591 0 0 0 60982 27 0 0 25 0 1 0 479983228 49336320 11546 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12045 11546 603 41 0 12004 0 vsize: 48180 [startup+620.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11685 0 0 0 61982 27 0 0 25 0 1 0 479983228 49684480 11640 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12130 11640 603 41 0 12089 0 vsize: 48520 [startup+630.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11685 0 0 0 62982 27 0 0 25 0 1 0 479983228 49684480 11640 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12130 11640 603 41 0 12089 0 vsize: 48520 [startup+640.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11686 0 0 0 63982 27 0 0 25 0 1 0 479983228 49684480 11641 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12130 11641 603 41 0 12089 0 vsize: 48520 [startup+650.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11687 0 0 0 64982 27 0 0 25 0 1 0 479983228 49684480 11642 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12130 11642 603 41 0 12089 0 vsize: 48520 [startup+660.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11687 0 0 0 65982 27 0 0 25 0 1 0 479983228 49684480 11642 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12130 11642 603 41 0 12089 0 vsize: 48520 [startup+670.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11688 0 0 0 66983 27 0 0 25 0 1 0 479983228 49684480 11643 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12130 11643 603 41 0 12089 0 vsize: 48520 [startup+680.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11688 0 0 0 67983 27 0 0 25 0 1 0 479983228 49684480 11643 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12130 11643 603 41 0 12089 0 vsize: 48520 [startup+690.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11688 0 0 0 68983 27 0 0 25 0 1 0 479983228 49664000 11642 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12125 11642 603 41 0 12084 0 vsize: 48500 [startup+700.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11688 0 0 0 69983 27 0 0 25 0 1 0 479983228 49664000 11642 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12125 11642 603 41 0 12084 0 vsize: 48500 [startup+710.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11688 0 0 0 70984 27 0 0 25 0 1 0 479983228 49664000 11642 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12125 11642 603 41 0 12084 0 vsize: 48500 [startup+720.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11921 0 0 0 71983 28 0 0 25 0 1 0 479983228 50638848 11874 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12363 11874 603 41 0 12322 0 vsize: 49452 [startup+722.904 s] Raw data (loadavg): 1.00 0.99 0.91 1/53 31808 Raw data (stat): 31808 (minisat+) R 31807 27222 27221 0 -1 0 11921 0 0 0 71983 28 0 0 25 0 1 0 479983228 50638848 11874 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12363 11874 603 41 0 12322 0 vsize: 0 Child status: 30 Real time (s): 722.903 CPU time (s): 723.007 CPU user time (s): 722.691 CPU system time (s): 0.315951 CPU usage (%): 100.014 Max. virtual memory (Kb): 49452 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####