Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl10_20_pb.cnf.cr.opb |
MD5SUM | f6063d1ff7b0ba7c7cab7a438daedff8 |
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 | 21 |
Number of bits of the biggest sum of numbers | 5 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.013997 |
Number of variables | 400 |
Total number of constraints | 60 |
Number of constraints which are clauses | 40 |
Number of constraints which are cardinality constraints (but not clauses) | 20 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 10 |
Maximum length of a constraint | 20 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc7 THE 2005-04-14 03:20:54 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4516 boxname=wulflinc7 idbench=4 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: f6063d1ff7b0ba7c7cab7a438daedff8 /oldhome/oroussel/tmp/wulflinc7/normalized-chnl10_20_pb.cnf.cr.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc7/normalized-chnl10_20_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc7/normalized-chnl10_20_pb.cnf.cr.opb IDLAUNCH: 4516 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 874796 kB Buffers: 38068 kB Cached: 102216 kB SwapCached: 0 kB Active: 73044 kB Inactive: 70092 kB HighTotal: 131008 kB HighFree: 24976 kB LowTotal: 903652 kB LowFree: 849820 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6924 kB Slab: 11140 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 03:30:28 (client local time) WITH STATUS 20 IN 574.495 SECONDS stats: 4516 7 574.495 20 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 60 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................ c ---[ 19]---> BDD-cost: 37 c ---[ 18]---> BDD-cost: 37 c ---[ 17]---> BDD-cost: 37 c ---[ 16]---> BDD-cost: 37 c ---[ 15]---> BDD-cost: 37 c ---[ 14]---> BDD-cost: 37 c ---[ 13]---> BDD-cost: 37 c ---[ 12]---> BDD-cost: 37 c ---[ 11]---> BDD-cost: 37 c ---[ 10]---> BDD-cost: 37 c ---[ 9]---> BDD-cost: 37 c ---[ 8]---> BDD-cost: 37 c ---[ 7]---> BDD-cost: 37 c ---[ 6]---> BDD-cost: 37 c ---[ 5]---> BDD-cost: 37 c ---[ 4]---> BDD-cost: 37 c ---[ 3]---> BDD-cost: 37 c ---[ 2]---> BDD-cost: 37 c ---[ 1]---> BDD-cost: 37 c ---[ 0]---> BDD-cost: 37 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 3280 9360 | 1093 0 0 nan | 0.000 % | c | 101 | 3280 9360 | 1202 101 2915 28.9 | 1.755 % | c | 252 | 3260 9300 | 1322 239 7471 31.3 | 2.105 % | c | 478 | 3245 9255 | 1454 459 16592 36.1 | 2.368 % | c | 820 | 3245 9255 | 1600 801 30818 38.5 | 2.368 % | c | 1326 | 3245 9255 | 1760 1307 55091 42.2 | 2.368 % | c | 2085 | 3245 9255 | 1936 1154 51269 44.4 | 2.368 % | c | 3226 | 3240 9240 | 2129 1236 51849 41.9 | 2.456 % | c | 4934 | 3225 9195 | 2342 1798 75430 42.0 | 2.719 % | c | 7496 | 3225 9195 | 2577 1814 69493 38.3 | 2.719 % | c | 11343 | 3200 9120 | 2834 1606 62746 39.1 | 3.158 % | c | 17111 | 3155 8985 | 3118 2868 116694 40.7 | 3.947 % | c | 25760 | 3125 8895 | 3430 3192 126058 39.5 | 4.474 % | c | 38734 | 3060 8700 | 3773 3437 141397 41.1 | 5.614 % | c | 58198 | 3005 8535 | 4150 3011 112566 37.4 | 6.579 % | c | 87393 | 2870 8130 | 4565 3601 159560 44.3 | 8.948 % | c | 131186 | 2580 7260 | 5022 3664 159479 43.5 | 14.035 % | c | 196871 | 2270 6330 | 5524 4969 208819 42.0 | 19.474 % | c | 295397 | 1980 5460 | 6076 5913 201464 34.1 | 24.561 % | c | 443186 | 1795 4905 | 6684 4069 173551 42.7 | 27.807 % | c | 664870 | 1675 4545 | 7353 4113 148008 36.0 | 29.912 % | c ============================================================================== c [1mUNSATISFIABLE[0m s UNKNOWN c _______________________________________________________________________________ c c restarts : 21 c conflicts : 974486 (1697 /sec) c decisions : 1162426 (2024 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 574.392 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.91 0.95 0.90 2/54 28740 Raw data (stat): 28740 (runsolver) R 28739 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423090175 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0003 s] Raw data (loadavg): 0.93 0.95 0.90 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 668 0 0 0 996 1 0 0 25 0 1 0 423090175 4304896 646 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1051 646 603 41 0 1010 0 vsize: 4204 [startup+20.0014 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 741 0 0 0 1995 2 0 0 25 0 1 0 423090175 4583424 719 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1119 719 603 41 0 1078 0 vsize: 4476 [startup+30.002 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 817 0 0 0 2995 2 0 0 25 0 1 0 423090175 4874240 795 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1190 795 603 41 0 1149 0 vsize: 4760 [startup+40.0022 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 887 0 0 0 3994 3 0 0 25 0 1 0 423090175 5279744 865 4294967295 134512640 134672761 3221224544 3221223728 134558629 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1289 865 603 41 0 1248 0 vsize: 5156 [startup+50.0033 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 919 0 0 0 4993 4 0 0 25 0 1 0 423090175 5419008 897 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1323 897 603 41 0 1282 0 vsize: 5292 [startup+60.0039 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 944 0 0 0 5993 4 0 0 25 0 1 0 423090175 5558272 922 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1357 922 603 41 0 1316 0 vsize: 5428 [startup+70.0041 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 984 0 0 0 6992 5 0 0 25 0 1 0 423090175 5693440 962 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1390 962 603 41 0 1349 0 vsize: 5560 [startup+80.0051 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1053 0 0 0 7991 6 0 0 25 0 1 0 423090175 5967872 1031 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1457 1031 603 41 0 1416 0 vsize: 5828 [startup+90.0058 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1079 0 0 0 8991 6 0 0 25 0 1 0 423090175 6115328 1057 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1493 1057 603 41 0 1452 0 vsize: 5972 [startup+100.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1107 0 0 0 9990 7 0 0 25 0 1 0 423090175 6262784 1085 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1529 1085 603 41 0 1488 0 vsize: 6116 [startup+110.007 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1125 0 0 0 10990 7 0 0 25 0 1 0 423090175 6262784 1103 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1529 1103 603 41 0 1488 0 vsize: 6116 [startup+120.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1161 0 0 0 11989 8 0 0 25 0 1 0 423090175 6402048 1139 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1563 1139 603 41 0 1522 0 vsize: 6252 [startup+130.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1173 0 0 0 12989 8 0 0 25 0 1 0 423090175 6549504 1151 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1599 1151 603 41 0 1558 0 vsize: 6396 [startup+140.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1180 0 0 0 13989 8 0 0 25 0 1 0 423090175 6549504 1158 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1599 1158 603 41 0 1558 0 vsize: 6396 [startup+150.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1221 0 0 0 14990 8 0 0 25 0 1 0 423090175 6696960 1199 4294967295 134512640 134672761 3221224544 3221223712 134561706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1635 1199 603 41 0 1594 0 vsize: 6540 [startup+160.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1226 0 0 0 15990 8 0 0 25 0 1 0 423090175 6696960 1204 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1635 1204 603 41 0 1594 0 vsize: 6540 [startup+170.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1238 0 0 0 16990 8 0 0 25 0 1 0 423090175 6696960 1216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1635 1216 603 41 0 1594 0 vsize: 6540 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1250 0 0 0 17989 8 0 0 25 0 1 0 423090175 6844416 1228 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1671 1228 603 41 0 1630 0 vsize: 6684 [startup+190.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1259 0 0 0 18990 8 0 0 25 0 1 0 423090175 6844416 1237 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1671 1237 603 41 0 1630 0 vsize: 6684 [startup+200.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1265 0 0 0 19990 8 0 0 25 0 1 0 423090175 6844416 1243 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1671 1243 603 41 0 1630 0 vsize: 6684 [startup+210.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1277 0 0 0 20990 8 0 0 25 0 1 0 423090175 6979584 1255 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1704 1255 603 41 0 1663 0 vsize: 6816 [startup+220.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1290 0 0 0 21990 8 0 0 25 0 1 0 423090175 6979584 1268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1704 1268 603 41 0 1663 0 vsize: 6816 [startup+230.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1291 0 0 0 22990 8 0 0 25 0 1 0 423090175 6979584 1269 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1704 1269 603 41 0 1663 0 vsize: 6816 [startup+240.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1319 0 0 0 23990 8 0 0 25 0 1 0 423090175 7114752 1297 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1737 1297 603 41 0 1696 0 vsize: 6948 [startup+250.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1333 0 0 0 24990 8 0 0 25 0 1 0 423090175 7278592 1311 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1777 1311 603 41 0 1736 0 vsize: 7108 [startup+260.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1398 0 0 0 25991 8 0 0 25 0 1 0 423090175 7577600 1376 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1850 1376 603 41 0 1809 0 vsize: 7400 [startup+270.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1450 0 0 0 26991 8 0 0 25 0 1 0 423090175 7847936 1428 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1916 1428 603 41 0 1875 0 vsize: 7664 [startup+280.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1456 0 0 0 27991 8 0 0 25 0 1 0 423090175 7847936 1434 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1916 1434 603 41 0 1875 0 vsize: 7664 [startup+290.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1464 0 0 0 28991 8 0 0 25 0 1 0 423090175 7847936 1442 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1916 1442 603 41 0 1875 0 vsize: 7664 [startup+300.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1496 0 0 0 29991 8 0 0 25 0 1 0 423090175 8011776 1474 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1956 1474 603 41 0 1915 0 vsize: 7824 [startup+310.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1506 0 0 0 30991 8 0 0 25 0 1 0 423090175 8175616 1484 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1996 1484 603 41 0 1955 0 vsize: 7984 [startup+320.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1506 0 0 0 31992 8 0 0 25 0 1 0 423090175 8175616 1484 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1996 1484 603 41 0 1955 0 vsize: 7984 [startup+330.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1512 0 0 0 32992 8 0 0 25 0 1 0 423090175 8175616 1490 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1996 1490 603 41 0 1955 0 vsize: 7984 [startup+340.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1540 0 0 0 33992 8 0 0 25 0 1 0 423090175 8310784 1518 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2029 1518 603 41 0 1988 0 vsize: 8116 [startup+350.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1552 0 0 0 34992 8 0 0 25 0 1 0 423090175 8310784 1530 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2029 1530 603 41 0 1988 0 vsize: 8116 [startup+360.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1559 0 0 0 35992 8 0 0 25 0 1 0 423090175 8454144 1537 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2064 1537 603 41 0 2023 0 vsize: 8256 [startup+370.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1565 0 0 0 36992 8 0 0 25 0 1 0 423090175 8454144 1543 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2064 1543 603 41 0 2023 0 vsize: 8256 [startup+380.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1576 0 0 0 37993 8 0 0 25 0 1 0 423090175 8454144 1554 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2064 1554 603 41 0 2023 0 vsize: 8256 [startup+390.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1584 0 0 0 38992 8 0 0 25 0 1 0 423090175 8454144 1562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2064 1562 603 41 0 2023 0 vsize: 8256 [startup+400.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1592 0 0 0 39991 9 0 0 25 0 1 0 423090175 8617984 1570 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2104 1570 603 41 0 2063 0 vsize: 8416 [startup+410.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1598 0 0 0 40991 9 0 0 25 0 1 0 423090175 8617984 1576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2104 1576 603 41 0 2063 0 vsize: 8416 [startup+420.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1617 0 0 0 41992 9 0 0 25 0 1 0 423090175 8617984 1595 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2104 1595 603 41 0 2063 0 vsize: 8416 [startup+430.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1623 0 0 0 42992 9 0 0 25 0 1 0 423090175 8781824 1601 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2144 1601 603 41 0 2103 0 vsize: 8576 [startup+440.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1628 0 0 0 43992 9 0 0 25 0 1 0 423090175 8781824 1606 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2144 1606 603 41 0 2103 0 vsize: 8576 [startup+450.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1628 0 0 0 44992 9 0 0 25 0 1 0 423090175 8781824 1606 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2144 1606 603 41 0 2103 0 vsize: 8576 [startup+460.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1634 0 0 0 45992 9 0 0 25 0 1 0 423090175 8781824 1612 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2144 1612 603 41 0 2103 0 vsize: 8576 [startup+470.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1644 0 0 0 46992 9 0 0 25 0 1 0 423090175 8781824 1622 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2144 1622 603 41 0 2103 0 vsize: 8576 [startup+480.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1650 0 0 0 47993 9 0 0 25 0 1 0 423090175 8945664 1628 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2184 1628 603 41 0 2143 0 vsize: 8736 [startup+490.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1668 0 0 0 48993 9 0 0 25 0 1 0 423090175 8945664 1646 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2184 1646 603 41 0 2143 0 vsize: 8736 [startup+500.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1673 0 0 0 49993 9 0 0 25 0 1 0 423090175 8945664 1651 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2184 1651 603 41 0 2143 0 vsize: 8736 [startup+510.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1679 0 0 0 50993 9 0 0 25 0 1 0 423090175 9109504 1657 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2224 1657 603 41 0 2183 0 vsize: 8896 [startup+520.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1696 0 0 0 51993 9 0 0 25 0 1 0 423090175 9109504 1674 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2224 1674 603 41 0 2183 0 vsize: 8896 [startup+530.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1697 0 0 0 52994 9 0 0 25 0 1 0 423090175 9109504 1675 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2224 1675 603 41 0 2183 0 vsize: 8896 [startup+540.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1709 0 0 0 53994 9 0 0 25 0 1 0 423090175 9273344 1687 4294967295 134512640 134672761 3221224544 3221223704 134561240 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2264 1687 603 41 0 2223 0 vsize: 9056 [startup+550.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1709 0 0 0 54994 9 0 0 25 0 1 0 423090175 9273344 1687 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2264 1687 603 41 0 2223 0 vsize: 9056 [startup+560.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1716 0 0 0 55994 9 0 0 25 0 1 0 423090175 9273344 1694 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2264 1694 603 41 0 2223 0 vsize: 9056 [startup+570.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1722 0 0 0 56994 9 0 0 25 0 1 0 423090175 9273344 1700 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2264 1700 603 41 0 2223 0 vsize: 9056 [startup+574.464 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 28740 Raw data (stat): 28740 (minisat+) R 28739 22932 22931 0 -1 0 1722 0 0 0 56994 9 0 0 25 0 1 0 423090175 9273344 1700 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2264 1700 603 41 0 2223 0 vsize: 0 Child status: 20 Real time (s): 574.464 CPU time (s): 574.495 CPU user time (s): 574.393 CPU system time (s): 0.101984 CPU usage (%): 100.005 Max. virtual memory (Kb): 9056 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####