Name | normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cc.opb |
MD5SUM | 0493ba9e257fafbb54efa7af2eeb7bf2 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1567 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 133 |
Biggest coefficient in the objective function | 60 |
Number of bits for the biggest coefficient in the objective function | 6 |
Sum of the numbers in the objective function | 5699 |
Number of bits of the sum of numbers in the objective function | 13 |
Biggest number in a constraint | 60 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 5699 |
Number of bits of the biggest sum of numbers | 13 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.134979 |
Number of variables | 133 |
Total number of constraints | 229 |
Number of constraints which are clauses | 229 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 31 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc12 THE 2005-04-13 21:11:58 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2255 boxname=wulflinc12 idbench=251 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 0493ba9e257fafbb54efa7af2eeb7bf2 /oldhome/oroussel/tmp/wulflinc12/normalized-cc.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc12/normalized-cc.opb IDLAUNCH: 2255 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 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 : 2 cpu MHz : 451.091 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: 920964 kB Buffers: 34676 kB Cached: 59964 kB SwapCached: 16 kB Active: 59104 kB Inactive: 38412 kB HighTotal: 131008 kB HighFree: 67116 kB LowTotal: 903652 kB LowFree: 853848 kB SwapTotal: 2097136 kB SwapFree: 2097120 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6920 kB Slab: 10644 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 21:32:00 (client local time) WITH STATUS 10 IN 1200.05 SECONDS stats: 2255 7 1200.05 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 199 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 197 772 | 65 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 1846[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:10637 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 23652 55574 | 7884 0 0 nan | 0.000 % | c | 101 | 23607 55480 | 8672 100 739 7.4 | 0.303 % | c | 253 | 23607 55480 | 9539 252 1980 7.9 | 0.304 % | c | 479 | 23461 55153 | 10493 470 4112 8.7 | 0.715 % | c | 817 | 23461 55153 | 11542 808 23124 28.6 | 0.715 % | c | 1324 | 23390 54993 | 12697 1309 32152 24.6 | 0.954 % | c ============================================================================== c [1mFound solution: 1819[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1541 | 23584 55524 | 7861 1525 35890 23.5 | 0.954 % | c | 1641 | 23584 55524 | 8647 1625 37279 22.9 | 0.975 % | c | 1791 | 23584 55524 | 9511 1775 48320 27.2 | 0.975 % | c ============================================================================== c [1mFound solution: 1816[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1928 | 23589 55542 | 7863 1912 52144 27.3 | 0.975 % | c ============================================================================== c [1mFound solution: 1760[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2000 | 23541 55436 | 7847 1977 53026 26.8 | 0.975 % | c | 2102 | 23541 55436 | 8631 2079 56552 27.2 | 1.220 % | c | 2252 | 23541 55436 | 9494 2229 66629 29.9 | 1.220 % | c | 2478 | 23541 55436 | 10444 2455 80579 32.8 | 1.220 % | c | 2815 | 23541 55436 | 11488 2792 90211 32.3 | 1.220 % | c | 3321 | 23541 55436 | 12637 3298 122096 37.0 | 1.220 % | c | 4081 | 23541 55436 | 13901 4058 134982 33.3 | 1.220 % | c | 5221 | 23541 55436 | 15291 5198 172493 33.2 | 1.220 % | c | 6930 | 23541 55436 | 16820 6907 288316 41.7 | 1.220 % | c | 9492 | 23541 55436 | 18502 9469 347250 36.7 | 1.220 % | c | 13337 | 23541 55436 | 20353 13314 653004 49.0 | 1.220 % | c | 19103 | 23541 55436 | 22388 19080 1024357 53.7 | 1.220 % | c ============================================================================== c [1mFound solution: 1731[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19218 | 23678 55796 | 7892 19195 1027813 53.5 | 1.220 % | c ============================================================================== c [1mFound solution: 1693[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19301 | 23689 55852 | 7896 4882 258270 52.9 | 1.220 % | c | 19401 | 23689 55852 | 8685 4982 263869 53.0 | 1.251 % | c | 19551 | 23689 55852 | 9554 5132 267144 52.1 | 1.251 % | c | 19776 | 23689 55852 | 10509 5357 285175 53.2 | 1.251 % | c | 20116 | 23689 55852 | 11560 5697 295627 51.9 | 1.251 % | c | 20624 | 23689 55852 | 12716 6205 316292 51.0 | 1.251 % | c | 21385 | 23689 55852 | 13988 6966 351890 50.5 | 1.251 % | c | 22524 | 23689 55852 | 15387 8105 406290 50.1 | 1.251 % | c | 24239 | 23689 55852 | 16925 9820 481842 49.1 | 1.251 % | c | 26802 | 23689 55852 | 18618 12383 610593 49.3 | 1.251 % | c | 30646 | 23689 55852 | 20480 16227 886767 54.6 | 1.251 % | c | 36413 | 23665 55799 | 22528 11355 488645 43.0 | 1.335 % | c ============================================================================== c [1mFound solution: 1688[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40664 | 23674 55865 | 7891 15606 741288 47.5 | 1.335 % | c ============================================================================== c [1mFound solution: 1679[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40687 | 23679 55878 | 7893 7826 331922 42.4 | 1.335 % | c | 40787 | 23679 55878 | 8682 7926 333913 42.1 | 1.355 % | c | 40938 | 23679 55878 | 9550 8077 342378 42.4 | 1.355 % | c | 41163 | 23679 55878 | 10505 8302 357891 43.1 | 1.355 % | c | 41501 | 23679 55878 | 11556 8640 379272 43.9 | 1.355 % | c | 42008 | 23679 55878 | 12711 9147 416772 45.6 | 1.355 % | c | 42767 | 23675 55869 | 13982 9901 445961 45.0 | 1.366 % | c | 43906 | 23675 55869 | 15381 11040 512916 46.5 | 1.366 % | c | 45616 | 23667 55853 | 16919 12746 598834 47.0 | 1.408 % | c | 48178 | 23667 55853 | 18611 15308 693981 45.3 | 1.408 % | c | 52022 | 23667 55853 | 20472 19152 959983 50.1 | 1.408 % | c | 57789 | 23667 55853 | 22519 13640 627202 46.0 | 1.408 % | c | 66438 | 23667 55853 | 24771 22289 1218970 54.7 | 1.408 % | c | 79412 | 23667 55853 | 27248 22217 1222636 55.0 | 1.408 % | c ============================================================================== c [1mFound solution: 1633[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 89499 | 23688 55912 | 7896 17467 750810 43.0 | 1.408 % | c | 89600 | 23688 55912 | 8685 4470 131522 29.4 | 1.417 % | c | 89750 | 23688 55912 | 9554 4620 139225 30.1 | 1.417 % | c | 89975 | 23682 55900 | 10509 4844 153049 31.6 | 1.448 % | c | 90312 | 23682 55900 | 11560 5181 171167 33.0 | 1.448 % | c | 90818 | 23660 55850 | 12716 5685 187037 32.9 | 1.544 % | c | 91579 | 23660 55850 | 13988 6446 206247 32.0 | 1.544 % | c | 92720 | 23660 55850 | 15387 7587 293552 38.7 | 1.544 % | c | 94430 | 23660 55850 | 16925 9297 336282 36.2 | 1.544 % | c | 96993 | 23660 55850 | 18618 11860 427336 36.0 | 1.544 % | c | 100837 | 23646 55818 | 20480 15691 582488 37.1 | 1.586 % | c | 106605 | 23646 55818 | 22528 21459 805228 37.5 | 1.586 % | c | 115255 | 23646 55818 | 24781 17976 609237 33.9 | 1.586 % | c | 128230 | 23646 55818 | 27259 17813 628007 35.3 | 1.586 % | c | 147691 | 23646 55818 | 29985 23003 702842 30.6 | 1.586 % | c | 176885 | 23646 55818 | 32983 18811 650416 34.6 | 1.586 % | c | 220674 | 23646 55818 | 36281 22829 1310770 57.4 | 1.586 % | c | 286359 | 23646 55818 | 39910 19503 943184 48.4 | 1.586 % | c | 384885 | 23646 55818 | 43901 34851 1504695 43.2 | 1.586 % | #### 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.85 0.95 0.90 2/54 28164 Raw data (stat): 28164 (runsolver) R 28163 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420868874 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0011 s] Raw data (loadavg): 0.87 0.95 0.90 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 1447 0 0 0 994 4 0 0 25 0 1 0 420868874 7888896 1407 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1926 1407 603 41 0 1885 0 vsize: 7704 [startup+20.0029 s] Raw data (loadavg): 0.89 0.96 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 1767 0 0 0 1993 5 0 0 25 0 1 0 420868874 9084928 1727 4294967295 134512640 134672761 3221224640 3221223744 134559877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2218 1727 603 41 0 2177 0 vsize: 8872 [startup+30.0031 s] Raw data (loadavg): 0.91 0.96 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 2176 0 0 0 2991 7 0 0 25 0 1 0 420868874 10883072 2136 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2657 2136 603 41 0 2616 0 vsize: 10628 [startup+40.0032 s] Raw data (loadavg): 0.92 0.96 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 2341 0 0 0 3990 7 0 0 25 0 1 0 420868874 11493376 2301 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2806 2301 603 41 0 2765 0 vsize: 11224 [startup+50.0041 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 2341 0 0 0 4991 7 0 0 25 0 1 0 420868874 11493376 2301 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2806 2301 603 41 0 2765 0 vsize: 11224 [startup+60.0036 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 2341 0 0 0 5991 7 0 0 25 0 1 0 420868874 11493376 2301 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2806 2301 603 41 0 2765 0 vsize: 11224 [startup+70.0048 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 2434 0 0 0 6991 8 0 0 25 0 1 0 420868874 11886592 2394 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2902 2394 603 41 0 2861 0 vsize: 11608 [startup+80.0056 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 2449 0 0 0 7991 8 0 0 25 0 1 0 420868874 11976704 2409 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2924 2409 603 41 0 2883 0 vsize: 11696 [startup+90.0051 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 2449 0 0 0 8991 8 0 0 25 0 1 0 420868874 11976704 2409 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2924 2409 603 41 0 2883 0 vsize: 11696 [startup+100.005 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 2449 0 0 0 9991 8 0 0 25 0 1 0 420868874 11976704 2409 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2924 2409 603 41 0 2883 0 vsize: 11696 [startup+110.006 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 2557 0 0 0 10991 8 0 0 25 0 1 0 420868874 12374016 2517 4294967295 134512640 134672761 3221224640 3221223824 134559031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3021 2517 603 41 0 2980 0 vsize: 12084 [startup+120.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 2559 0 0 0 11991 8 0 0 25 0 1 0 420868874 12374016 2519 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3021 2519 603 41 0 2980 0 vsize: 12084 [startup+130.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 2733 0 0 0 12991 8 0 0 25 0 1 0 420868874 13180928 2693 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3218 2693 603 41 0 3177 0 vsize: 12872 [startup+140.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3005 0 0 0 13990 9 0 0 25 0 1 0 420868874 14254080 2965 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3480 2965 603 41 0 3439 0 vsize: 13920 [startup+150.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3008 0 0 0 14991 9 0 0 25 0 1 0 420868874 14254080 2968 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3480 2968 603 41 0 3439 0 vsize: 13920 [startup+160.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3008 0 0 0 15991 9 0 0 25 0 1 0 420868874 14254080 2968 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3480 2968 603 41 0 3439 0 vsize: 13920 [startup+170.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3008 0 0 0 16989 10 0 0 25 0 1 0 420868874 14254080 2968 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3480 2968 603 41 0 3439 0 vsize: 13920 [startup+180.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3068 0 0 0 17988 10 0 0 25 0 1 0 420868874 14524416 3028 4294967295 134512640 134672761 3221224640 3221223776 134560604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3028 603 41 0 3505 0 vsize: 14184 [startup+190.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3068 0 0 0 18989 10 0 0 25 0 1 0 420868874 14524416 3028 4294967295 134512640 134672761 3221224640 3221223840 134557800 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3028 603 41 0 3505 0 vsize: 14184 [startup+200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3068 0 0 0 19989 10 0 0 25 0 1 0 420868874 14524416 3028 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3028 603 41 0 3505 0 vsize: 14184 [startup+210.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3068 0 0 0 20989 10 0 0 25 0 1 0 420868874 14524416 3028 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3028 603 41 0 3505 0 vsize: 14184 [startup+220.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3068 0 0 0 21989 10 0 0 25 0 1 0 420868874 14524416 3028 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3028 603 41 0 3505 0 vsize: 14184 [startup+230.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3068 0 0 0 22989 10 0 0 25 0 1 0 420868874 14524416 3028 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3028 603 41 0 3505 0 vsize: 14184 [startup+240.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3068 0 0 0 23989 10 0 0 25 0 1 0 420868874 14524416 3028 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3028 603 41 0 3505 0 vsize: 14184 [startup+250.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3068 0 0 0 24990 10 0 0 25 0 1 0 420868874 14524416 3028 4294967295 134512640 134672761 3221224640 3221223808 134561127 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3028 603 41 0 3505 0 vsize: 14184 [startup+260.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3068 0 0 0 25990 10 0 0 25 0 1 0 420868874 14524416 3028 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3028 603 41 0 3505 0 vsize: 14184 [startup+270.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3068 0 0 0 26990 10 0 0 25 0 1 0 420868874 14524416 3028 4294967295 134512640 134672761 3221224640 3221223808 134561256 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3028 603 41 0 3505 0 vsize: 14184 [startup+280.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3068 0 0 0 27990 10 0 0 25 0 1 0 420868874 14524416 3028 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3028 603 41 0 3505 0 vsize: 14184 [startup+290.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3068 0 0 0 28990 10 0 0 25 0 1 0 420868874 14524416 3028 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3028 603 41 0 3505 0 vsize: 14184 [startup+300.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3069 0 0 0 29991 10 0 0 25 0 1 0 420868874 14524416 3029 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3029 603 41 0 3505 0 vsize: 14184 [startup+310.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3069 0 0 0 30991 10 0 0 25 0 1 0 420868874 14524416 3029 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3029 603 41 0 3505 0 vsize: 14184 [startup+320.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3069 0 0 0 31991 10 0 0 25 0 1 0 420868874 14524416 3029 4294967295 134512640 134672761 3221224640 3221223824 134559542 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3029 603 41 0 3505 0 vsize: 14184 [startup+330.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3069 0 0 0 32991 10 0 0 25 0 1 0 420868874 14524416 3029 4294967295 134512640 134672761 3221224640 3221223788 134565030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3029 603 41 0 3505 0 vsize: 14184 [startup+340.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3069 0 0 0 33991 10 0 0 25 0 1 0 420868874 14524416 3029 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3029 603 41 0 3505 0 vsize: 14184 [startup+350.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3071 0 0 0 34992 10 0 0 25 0 1 0 420868874 14524416 3031 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3031 603 41 0 3505 0 vsize: 14184 [startup+360.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3072 0 0 0 35992 10 0 0 25 0 1 0 420868874 14524416 3032 4294967295 134512640 134672761 3221224640 3221223824 134559594 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3032 603 41 0 3505 0 vsize: 14184 [startup+370.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3072 0 0 0 36992 10 0 0 25 0 1 0 420868874 14524416 3032 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3032 603 41 0 3505 0 vsize: 14184 [startup+380.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3072 0 0 0 37992 10 0 0 25 0 1 0 420868874 14524416 3032 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3032 603 41 0 3505 0 vsize: 14184 [startup+390.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3072 0 0 0 38992 10 0 0 25 0 1 0 420868874 14524416 3032 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3032 603 41 0 3505 0 vsize: 14184 [startup+400.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3082 0 0 0 39993 10 0 0 25 0 1 0 420868874 14524416 3042 4294967295 134512640 134672761 3221224640 3221223360 134565768 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3042 603 41 0 3505 0 vsize: 14184 [startup+410.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3082 0 0 0 40993 10 0 0 25 0 1 0 420868874 14524416 3042 4294967295 134512640 134672761 3221224640 3221223800 134561238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3042 603 41 0 3505 0 vsize: 14184 [startup+420.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3082 0 0 0 41993 10 0 0 25 0 1 0 420868874 14524416 3042 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3042 603 41 0 3505 0 vsize: 14184 [startup+430.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3088 0 0 0 42993 10 0 0 25 0 1 0 420868874 14524416 3048 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3546 3048 603 41 0 3505 0 vsize: 14184 [startup+440.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3326 0 0 0 43992 11 0 0 25 0 1 0 420868874 15581184 3286 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3804 3286 603 41 0 3763 0 vsize: 15216 [startup+450.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3579 0 0 0 44991 12 0 0 25 0 1 0 420868874 16769024 3539 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4094 3539 603 41 0 4053 0 vsize: 16376 [startup+460.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3586 0 0 0 45992 12 0 0 25 0 1 0 420868874 16769024 3546 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4094 3546 603 41 0 4053 0 vsize: 16376 [startup+470.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3610 0 0 0 46992 12 0 0 25 0 1 0 420868874 16908288 3570 4294967295 134512640 134672761 3221224640 3221223840 134557811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4128 3570 603 41 0 4087 0 vsize: 16512 [startup+480.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3610 0 0 0 47992 12 0 0 25 0 1 0 420868874 16908288 3570 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4128 3570 603 41 0 4087 0 vsize: 16512 [startup+490.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3733 0 0 0 48992 13 0 0 25 0 1 0 420868874 17309696 3693 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4226 3693 603 41 0 4185 0 vsize: 16904 [startup+500.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 3971 0 0 0 49991 13 0 0 25 0 1 0 420868874 18382848 3931 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4488 3931 603 41 0 4447 0 vsize: 17952 [startup+510.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4170 0 0 0 50991 14 0 0 25 0 1 0 420868874 19177472 4130 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4682 4130 603 41 0 4641 0 vsize: 18728 [startup+520.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4301 0 0 0 51991 14 0 0 25 0 1 0 420868874 19709952 4261 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4812 4261 603 41 0 4771 0 vsize: 19248 [startup+530.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4308 0 0 0 52991 14 0 0 25 0 1 0 420868874 19849216 4268 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4846 4268 603 41 0 4805 0 vsize: 19384 [startup+540.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4316 0 0 0 53991 14 0 0 25 0 1 0 420868874 19849216 4276 4294967295 134512640 134672761 3221224640 3221223792 134565153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4846 4276 603 41 0 4805 0 vsize: 19384 [startup+550.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4322 0 0 0 54991 14 0 0 25 0 1 0 420868874 19849216 4282 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4846 4282 603 41 0 4805 0 vsize: 19384 [startup+560.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4322 0 0 0 55990 14 0 0 25 0 1 0 420868874 19849216 4282 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4846 4282 603 41 0 4805 0 vsize: 19384 [startup+570.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4322 0 0 0 56990 15 0 0 25 0 1 0 420868874 19849216 4282 4294967295 134512640 134672761 3221224640 3221223744 134560379 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4846 4282 603 41 0 4805 0 vsize: 19384 [startup+580.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4352 0 0 0 57990 15 0 0 25 0 1 0 420868874 19984384 4312 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4879 4312 603 41 0 4838 0 vsize: 19516 [startup+590.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4352 0 0 0 58989 15 0 0 25 0 1 0 420868874 19984384 4312 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4879 4312 603 41 0 4838 0 vsize: 19516 [startup+600.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4352 0 0 0 59989 15 0 0 25 0 1 0 420868874 19984384 4312 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4879 4312 603 41 0 4838 0 vsize: 19516 [startup+610.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4364 0 0 0 60988 16 0 0 25 0 1 0 420868874 19984384 4324 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4879 4324 603 41 0 4838 0 vsize: 19516 [startup+620.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4370 0 0 0 61988 16 0 0 25 0 1 0 420868874 20123648 4330 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4913 4330 603 41 0 4872 0 vsize: 19652 [startup+630.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4378 0 0 0 62988 16 0 0 25 0 1 0 420868874 20123648 4338 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4913 4338 603 41 0 4872 0 vsize: 19652 [startup+640.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4394 0 0 0 63988 16 0 0 25 0 1 0 420868874 20123648 4354 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4913 4354 603 41 0 4872 0 vsize: 19652 [startup+650.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4395 0 0 0 64987 17 0 0 25 0 1 0 420868874 20123648 4355 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4913 4355 603 41 0 4872 0 vsize: 19652 [startup+660.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4395 0 0 0 65987 17 0 0 25 0 1 0 420868874 20123648 4355 4294967295 134512640 134672761 3221224640 3221223744 134560410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4913 4355 603 41 0 4872 0 vsize: 19652 [startup+670.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4395 0 0 0 66987 17 0 0 25 0 1 0 420868874 20123648 4355 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4913 4355 603 41 0 4872 0 vsize: 19652 [startup+680.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4395 0 0 0 67986 18 0 0 25 0 1 0 420868874 20123648 4355 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4913 4355 603 41 0 4872 0 vsize: 19652 [startup+690.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4396 0 0 0 68986 18 0 0 25 0 1 0 420868874 20123648 4356 4294967295 134512640 134672761 3221224640 3221223744 134560191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4913 4356 603 41 0 4872 0 vsize: 19652 [startup+700.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4401 0 0 0 69986 18 0 0 25 0 1 0 420868874 20123648 4361 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4913 4361 603 41 0 4872 0 vsize: 19652 [startup+710.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4404 0 0 0 70985 18 0 0 25 0 1 0 420868874 20271104 4364 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4949 4364 603 41 0 4908 0 vsize: 19796 [startup+720.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4404 0 0 0 71985 19 0 0 25 0 1 0 420868874 20271104 4364 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4949 4364 603 41 0 4908 0 vsize: 19796 [startup+730.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4419 0 0 0 72985 19 0 0 25 0 1 0 420868874 20271104 4379 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4949 4379 603 41 0 4908 0 vsize: 19796 [startup+740.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4420 0 0 0 73984 19 0 0 25 0 1 0 420868874 20271104 4380 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4949 4380 603 41 0 4908 0 vsize: 19796 [startup+750.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4427 0 0 0 74983 20 0 0 25 0 1 0 420868874 20271104 4387 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4949 4387 603 41 0 4908 0 vsize: 19796 [startup+760.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4443 0 0 0 75983 20 0 0 25 0 1 0 420868874 20430848 4403 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4988 4403 603 41 0 4947 0 vsize: 19952 [startup+770.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4444 0 0 0 76983 20 0 0 25 0 1 0 420868874 20430848 4404 4294967295 134512640 134672761 3221224640 3221223840 134557887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4988 4404 603 41 0 4947 0 vsize: 19952 [startup+780.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4444 0 0 0 77982 21 0 0 25 0 1 0 420868874 20430848 4404 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4988 4404 603 41 0 4947 0 vsize: 19952 [startup+790.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4446 0 0 0 78982 21 0 0 25 0 1 0 420868874 20430848 4406 4294967295 134512640 134672761 3221224640 3221223800 134561238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4988 4406 603 41 0 4947 0 vsize: 19952 [startup+800.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4458 0 0 0 79981 21 0 0 25 0 1 0 420868874 20430848 4418 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4988 4418 603 41 0 4947 0 vsize: 19952 [startup+810.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4471 0 0 0 80981 22 0 0 25 0 1 0 420868874 20594688 4431 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5028 4431 603 41 0 4987 0 vsize: 20112 [startup+820.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4479 0 0 0 81980 22 0 0 25 0 1 0 420868874 20594688 4439 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5028 4439 603 41 0 4987 0 vsize: 20112 [startup+830.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4480 0 0 0 82980 23 0 0 25 0 1 0 420868874 20594688 4440 4294967295 134512640 134672761 3221224640 3221223824 134558352 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5028 4440 603 41 0 4987 0 vsize: 20112 [startup+840.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4481 0 0 0 83980 23 0 0 25 0 1 0 420868874 20594688 4441 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5028 4441 603 41 0 4987 0 vsize: 20112 [startup+850.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4489 0 0 0 84979 23 0 0 25 0 1 0 420868874 20594688 4449 4294967295 134512640 134672761 3221224640 3221223808 134561003 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5028 4449 603 41 0 4987 0 vsize: 20112 [startup+860.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4489 0 0 0 85979 23 0 0 25 0 1 0 420868874 20594688 4449 4294967295 134512640 134672761 3221224640 3221223776 134560657 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5028 4449 603 41 0 4987 0 vsize: 20112 [startup+870.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4498 0 0 0 86979 24 0 0 25 0 1 0 420868874 20594688 4458 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5028 4458 603 41 0 4987 0 vsize: 20112 [startup+880.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4504 0 0 0 87979 24 0 0 25 0 1 0 420868874 20738048 4464 4294967295 134512640 134672761 3221224640 3221223824 134559330 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5063 4464 603 41 0 5022 0 vsize: 20252 [startup+890.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4504 0 0 0 88978 24 0 0 25 0 1 0 420868874 20738048 4464 4294967295 134512640 134672761 3221224640 3221223824 134559045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5063 4464 603 41 0 5022 0 vsize: 20252 [startup+900.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4515 0 0 0 89978 24 0 0 25 0 1 0 420868874 20738048 4475 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5063 4475 603 41 0 5022 0 vsize: 20252 [startup+910.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4532 0 0 0 90978 24 0 0 25 0 1 0 420868874 20901888 4492 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5103 4492 603 41 0 5062 0 vsize: 20412 [startup+920.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4532 0 0 0 91978 25 0 0 25 0 1 0 420868874 20901888 4492 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5103 4492 603 41 0 5062 0 vsize: 20412 [startup+930.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4532 0 0 0 92977 25 0 0 25 0 1 0 420868874 20901888 4492 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5103 4492 603 41 0 5062 0 vsize: 20412 [startup+940.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4550 0 0 0 93977 25 0 0 25 0 1 0 420868874 20901888 4510 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5103 4510 603 41 0 5062 0 vsize: 20412 [startup+950.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4550 0 0 0 94977 25 0 0 25 0 1 0 420868874 20901888 4510 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5103 4510 603 41 0 5062 0 vsize: 20412 [startup+960.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4550 0 0 0 95977 25 0 0 25 0 1 0 420868874 20901888 4510 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5103 4510 603 41 0 5062 0 vsize: 20412 [startup+970.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4550 0 0 0 96977 25 0 0 25 0 1 0 420868874 20901888 4510 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5103 4510 603 41 0 5062 0 vsize: 20412 [startup+980.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4550 0 0 0 97976 26 0 0 25 0 1 0 420868874 20901888 4510 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5103 4510 603 41 0 5062 0 vsize: 20412 [startup+990.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4559 0 0 0 98976 26 0 0 25 0 1 0 420868874 21049344 4519 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5139 4519 603 41 0 5098 0 vsize: 20556 [startup+1000.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4559 0 0 0 99975 26 0 0 25 0 1 0 420868874 21049344 4519 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5139 4519 603 41 0 5098 0 vsize: 20556 [startup+1010.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4559 0 0 0 100975 27 0 0 25 0 1 0 420868874 21049344 4519 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5139 4519 603 41 0 5098 0 vsize: 20556 [startup+1020.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4559 0 0 0 101975 27 0 0 25 0 1 0 420868874 21049344 4519 4294967295 134512640 134672761 3221224640 3221223808 134561261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5139 4519 603 41 0 5098 0 vsize: 20556 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4559 0 0 0 102975 27 0 0 25 0 1 0 420868874 21049344 4519 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5139 4519 603 41 0 5098 0 vsize: 20556 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4566 0 0 0 103974 27 0 0 25 0 1 0 420868874 21049344 4526 4294967295 134512640 134672761 3221224640 3221223808 134560845 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5139 4526 603 41 0 5098 0 vsize: 20556 [startup+1050.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4567 0 0 0 104974 27 0 0 25 0 1 0 420868874 21049344 4527 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5139 4527 603 41 0 5098 0 vsize: 20556 [startup+1060.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4573 0 0 0 105974 28 0 0 25 0 1 0 420868874 21049344 4533 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5139 4533 603 41 0 5098 0 vsize: 20556 [startup+1070.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4579 0 0 0 106973 28 0 0 25 0 1 0 420868874 21049344 4539 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5139 4539 603 41 0 5098 0 vsize: 20556 [startup+1080.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4579 0 0 0 107973 28 0 0 25 0 1 0 420868874 21049344 4539 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5139 4539 603 41 0 5098 0 vsize: 20556 [startup+1090.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4593 0 0 0 108973 29 0 0 25 0 1 0 420868874 21213184 4553 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5179 4553 603 41 0 5138 0 vsize: 20716 [startup+1100.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4593 0 0 0 109972 29 0 0 25 0 1 0 420868874 21213184 4553 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5179 4553 603 41 0 5138 0 vsize: 20716 [startup+1110.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4593 0 0 0 110972 29 0 0 25 0 1 0 420868874 21213184 4553 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5179 4553 603 41 0 5138 0 vsize: 20716 [startup+1120.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4604 0 0 0 111972 29 0 0 25 0 1 0 420868874 21213184 4564 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5179 4564 603 41 0 5138 0 vsize: 20716 [startup+1130.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4619 0 0 0 112972 29 0 0 25 0 1 0 420868874 21213184 4579 4294967295 134512640 134672761 3221224640 3221223744 134554662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5179 4579 603 41 0 5138 0 vsize: 20716 [startup+1140.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4619 0 0 0 113972 29 0 0 25 0 1 0 420868874 21213184 4579 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5179 4579 603 41 0 5138 0 vsize: 20716 [startup+1150.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4632 0 0 0 114972 30 0 0 25 0 1 0 420868874 21409792 4592 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5227 4592 603 41 0 5186 0 vsize: 20908 [startup+1160.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4633 0 0 0 115972 30 0 0 25 0 1 0 420868874 21409792 4593 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5227 4593 603 41 0 5186 0 vsize: 20908 [startup+1170.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4645 0 0 0 116973 30 0 0 25 0 1 0 420868874 21409792 4605 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5227 4605 603 41 0 5186 0 vsize: 20908 [startup+1180.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4647 0 0 0 117973 30 0 0 25 0 1 0 420868874 21409792 4607 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5227 4607 603 41 0 5186 0 vsize: 20908 [startup+1190.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4648 0 0 0 118973 30 0 0 25 0 1 0 420868874 21409792 4608 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5227 4608 603 41 0 5186 0 vsize: 20908 [startup+1200.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28164 Raw data (stat): 28164 (minisat+) R 28163 25285 25284 0 -1 0 4649 0 0 0 119973 30 0 0 25 0 1 0 420868874 21409792 4609 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5227 4609 603 41 0 5186 0 vsize: 20908 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 28164 Raw data (stat): 28164 (minisat+) Z 28163 25285 25284 0 -1 12 4652 0 0 0 119973 31 0 0 25 0 1 0 420868874 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.07 CPU time (s): 1200.05 CPU user time (s): 1199.74 CPU system time (s): 0.312952 CPU usage (%): 99.9981 Max. virtual memory (Kb): 20908 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####