Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-2.opb |
MD5SUM | 409f1cf0658f035df65cb61f3e4f598e |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -28 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 595 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 595 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 595 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.05 |
Number of variables | 595 |
Total number of constraints | 27847 |
Number of constraints which are clauses | 27847 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 2 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc32 THE 2005-04-14 00:50:39 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4080 boxname=wulflinc32 idbench=320 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 409f1cf0658f035df65cb61f3e4f598e /oldhome/oroussel/tmp/wulflinc32/normalized-frb35-17-2.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc32/normalized-frb35-17-2.opb /oldhome/oroussel/tmp/wulflinc32/normalized-frb35-17-2.opb IDLAUNCH: 4080 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.085 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.085 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: 1034724 kB MemFree: 707748 kB Buffers: 34940 kB Cached: 180292 kB SwapCached: 1212 kB Active: 146768 kB Inactive: 148824 kB HighTotal: 131072 kB HighFree: 256 kB LowTotal: 903652 kB LowFree: 707492 kB SwapTotal: 2097892 kB SwapFree: 2096680 kB Dirty: 2316 kB Writeback: 0 kB Mapped: 81768 kB Slab: 25660 kB Committed_AS: 174000 kB PageTables: 432 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 01:10:41 (client local time) WITH STATUS 10 IN 1200.18 SECONDS stats: 4080 7 1200.18 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 27847 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 27847 55694 | 8354 0 0 nan | 0.000 % | c -- subsuming c | 0 | 27847 55694 | 11138 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 1.09783 s) c ============================================================================== c [1mFound solution: -24[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:26814 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 56117 122092 | 16835 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/19331 c -- var.elim.: 2000/19331 c -- var.elim.: 3000/19331 c -- var.elim.: 4000/19331 c -- var.elim.: 5000/19331 c -- var.elim.: 6000/19331 c -- var.elim.: 7000/19331 c -- var.elim.: 8000/19331 c -- var.elim.: 9000/19331 c -- var.elim.: 10000/19331 c -- var.elim.: 11000/19331 c -- var.elim.: 12000/19331 c -- var.elim.: 13000/19331 c -- var.elim.: 14000/19331 c -- var.elim.: 15000/19331 c -- var.elim.: 16000/19331 c -- var.elim.: 17000/19331 c -- var.elim.: 18000/19331 c -- var.elim.: 19000/19331 c -- var.elim.: 19331/19331 c -- var.elim.: 1000/9850 c -- var.elim.: 2000/9850 c -- var.elim.: 3000/9850 c -- var.elim.: 4000/9850 c -- var.elim.: 5000/9850 c -- var.elim.: 6000/9850 c -- var.elim.: 7000/9850 c -- var.elim.: 8000/9850 c -- var.elim.: 9000/9850 c -- var.elim.: 9850/9850 c -- var.elim.: 85/85 c -- var.elim.: 37/37 c -- subsuming c -- var.elim.: 1000/3869 c -- var.elim.: 2000/3869 c -- var.elim.: 3000/3869 c -- var.elim.: 3869/3869 c -- var.elim.: 368/368 c | 0 | 36235 121913 | -- 0 -- -- | -- | -19877/-164 c | 0 | 36235 121913 | 14494 0 0 nan | 0.000 % | c | 100 | 36235 121913 | 15943 100 7380 73.8 | 52.610 % | c | 250 | 36235 121913 | 17537 250 24858 99.4 | 52.609 % | c | 476 | 36217 121759 | 19281 475 54042 113.8 | 52.701 % | c ============================================================================== c (current CPU-time: 39.393 s) c ============================================================================== c [1mFound solution: -25[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 794 | 39198 130032 | 11759 793 109586 138.2 | 52.701 % | c -- subsuming c -- var.elim.: 1000/6121 c -- var.elim.: 2000/6121 c -- var.elim.: 3000/6121 c -- var.elim.: 4000/6121 c -- var.elim.: 5000/6121 c -- var.elim.: 6000/6121 c -- var.elim.: 6121/6121 c -- var.elim.: 1000/2330 c -- var.elim.: 2000/2330 c -- var.elim.: 2330/2330 c | 794 | 36268 129241 | -- 793 -- -- | -- | -2930/-790 c | 794 | 36268 129241 | 14507 793 109586 138.2 | 52.701 % | c | 896 | 36268 129241 | 15957 895 124196 138.8 | 57.572 % | c | 1046 | 36268 129241 | 17553 1045 147458 141.1 | 57.572 % | c ============================================================================== c (current CPU-time: 47.8647 s) c ============================================================================== c [1mFound solution: -27[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1238 | 40360 140506 | 12107 1237 177620 143.6 | 57.572 % | c -- subsuming c -- var.elim.: 1000/7154 c -- var.elim.: 2000/7154 c -- var.elim.: 3000/7154 c -- var.elim.: 4000/7154 c -- var.elim.: 5000/7154 c -- var.elim.: 6000/7154 c -- var.elim.: 7000/7154 c -- var.elim.: 7154/7154 c -- var.elim.: 1000/3077 c -- var.elim.: 2000/3077 c -- var.elim.: 3000/3077 c -- var.elim.: 3077/3077 c -- var.elim.: 4/4 c | 1238 | 36365 137393 | -- 1237 -- -- | -- | -3989/-3100 c | 1238 | 36365 137393 | 14546 1237 177620 143.6 | 57.572 % | c | 1338 | 36365 137393 | 16000 1337 201478 150.7 | 58.405 % | c | 1488 | 36365 137393 | 17600 1487 215733 145.1 | 58.405 % | c | 1713 | 36331 137039 | 19342 1708 242983 142.3 | 58.530 % | c | 2050 | 36331 137039 | 21276 2045 285103 139.4 | 58.529 % | c | 2556 | 36301 136723 | 23385 2547 366271 143.8 | 58.663 % | c | 3316 | 36208 135828 | 25657 3304 485100 146.8 | 59.045 % | c | 4455 | 36064 134395 | 28111 4429 747700 168.8 | 59.640 % | c ============================================================================== c (current CPU-time: 68.6286 s) c ============================================================================== c [1mFound solution: -28[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 5508 | 36964 135284 | 11089 5455 951126 174.4 | 59.640 % | c -- subsuming c -- var.elim.: 1000/5404 c -- var.elim.: 2000/5404 c -- var.elim.: 3000/5404 c -- var.elim.: 4000/5404 c -- var.elim.: 5000/5404 c -- var.elim.: 5404/5404 c -- var.elim.: 1000/1040 c -- var.elim.: 1040/1040 c -- var.elim.: 2/2 c | 5508 | 35803 130124 | -- 5455 -- -- | -- | -1141/-3749 c | 5508 | 35803 130124 | 14321 4805 506080 105.3 | 59.640 % | c | 5609 | 35765 129783 | 15736 4904 523461 106.7 | 60.951 % | c | 5759 | 35711 129357 | 17284 5041 544500 108.0 | 61.137 % | c | 5984 | 35711 129357 | 19012 5266 585074 111.1 | 61.137 % | c | 6321 | 35711 129357 | 20913 5603 673444 120.2 | 61.137 % | c | 6828 | 35643 128764 | 22961 6105 778996 127.6 | 61.438 % | c | 7587 | 35593 128242 | 25222 6851 947237 138.3 | 61.659 % | c | 8726 | 35387 126387 | 27583 7955 1252575 157.5 | 62.571 % | c ============================================================================== c (current CPU-time: 84.0622 s) c ============================================================================== c [1mFound solution: -29[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 9128 | 36457 128779 | 10937 8338 1326901 159.1 | 62.571 % | c -- subsuming c -- var.elim.: 1000/5118 c -- var.elim.: 2000/5118 c -- var.elim.: 3000/5118 c -- var.elim.: 4000/5118 c -- var.elim.: 5000/5118 c -- var.elim.: 5118/5118 c -- var.elim.: 1000/1049 c -- var.elim.: 1049/1049 c | 9128 | 35313 126704 | -- 8338 -- -- | -- | -1144/-2074 c | 9128 | 35313 126704 | 14125 8338 1326901 159.1 | 62.571 % | c | 9228 | 35289 126463 | 15527 8437 1347624 159.7 | 63.383 % | c | 9378 | 35203 125635 | 17038 8529 1353604 158.7 | 63.761 % | c | 9604 | 35203 125635 | 18742 8755 1388335 158.6 | 63.761 % | c | 9941 | 35203 125635 | 20616 9092 1443829 158.8 | 63.761 % | c | 10447 | 35203 125635 | 22677 9598 1556268 162.1 | 63.761 % | c | 11206 | 35079 124486 | 24857 10316 1728682 167.6 | 64.306 % | c | 12345 | 35007 123721 | 27287 11440 2006539 175.4 | 64.622 % | c | 14053 | 34945 123025 | 29963 13113 2438571 186.0 | 64.886 % | c | 16615 | 34615 119966 | 32648 15550 2924835 188.1 | 66.318 % | c | 20459 | 34460 118517 | 35752 19348 3837785 198.4 | 66.968 % | c | 26225 | 34094 114797 | 38909 25002 5305831 212.2 | 68.541 % | c | 34874 | 33633 106887 | 42221 33464 7925738 236.8 | 70.466 % | c ============================================================================== c (current CPU-time: 183.911 s) c ============================================================================== c [1mFound solution: -30[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 38763 | 34235 106878 | 10270 37296 9163997 245.7 | 70.466 % | c -- subsuming c -- var.elim.: 1000/4076 c -- var.elim.: 2000/4076 c -- var.elim.: 3000/4076 c -- var.elim.: 4000/4076 c -- var.elim.: 4076/4076 c -- var.elim.: 1000/1910 c -- var.elim.: 1910/1910 c -- var.elim.: 1000/1059 c -- var.elim.: 1059/1059 c | 38763 | 33308 99097 | -- 37296 -- -- | -- | -897/-3012 c | 38763 | 33308 99097 | 13323 27231 3344817 122.8 | 70.466 % | c | 38863 | 33306 99077 | 14654 11908 1031719 86.6 | 72.307 % | c | 39013 | 33306 99077 | 16120 12058 1058540 87.8 | 72.307 % | c | 39238 | 33306 99077 | 17732 12283 1106448 90.1 | 72.307 % | c | 39575 | 33306 99077 | 19505 12620 1210413 95.9 | 72.307 % | c | 40081 | 33306 99077 | 21455 13126 1350205 102.9 | 72.307 % | c | 40841 | 33264 98763 | 23571 13876 1487989 107.2 | 72.480 % | c | 41980 | 33234 98522 | 25905 15006 1750061 116.6 | 72.602 % | c | 43689 | 33234 98522 | 28496 16715 2137835 127.9 | 72.602 % | c | 46252 | 33234 98522 | 31345 19278 2889509 149.9 | 72.602 % | c | 50096 | 33197 98175 | 34441 23112 3963958 171.5 | 72.749 % | c | 55863 | 32981 96218 | 37639 28847 5405803 187.4 | 73.660 % | c | 64512 | 32729 94099 | 41087 37364 7521912 201.3 | 74.692 % | c | 77489 | 32366 91043 | 44694 50150 10645711 212.3 | 76.202 % | c | 96950 | 31825 86736 | 48342 33498 6552759 195.6 | 78.413 % | c | 126142 | 31237 82423 | 52193 24202 3605631 149.0 | 80.850 % | c ============================================================================== c (current CPU-time: 507.527 s) c ============================================================================== c [1mFound solution: -31[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 136961 | 32974 86613 | 9892 34997 6322247 180.7 | 80.850 % | c -- subsuming c -- var.elim.: 1000/3918 c -- var.elim.: 2000/3918 c -- var.elim.: 3000/3918 c -- var.elim.: 3918/3918 c -- var.elim.: 1000/1132 c -- var.elim.: 1132/1132 c -- var.elim.: 4/4 c | 136961 | 31229 84045 | -- 34997 -- -- | -- | -1737/-2551 c | 136961 | 31229 84045 | 12491 28192 3976532 141.1 | 80.850 % | c | 137062 | 31229 84045 | 13740 14916 2147303 144.0 | 85.364 % | c | 137212 | 31229 84045 | 15114 15066 2177522 144.5 | 85.364 % | c | 137437 | 31229 84045 | 16626 15291 2214756 144.8 | 85.364 % | c | 137774 | 31229 84045 | 18288 15628 2285887 146.3 | 85.364 % | c | 138281 | 31229 84045 | 20117 16135 2394456 148.4 | 85.364 % | c | 139041 | 31229 84045 | 22129 16895 2545891 150.7 | 85.364 % | c | 140180 | 31229 84045 | 24342 18034 2773515 153.8 | 85.364 % | c | 141889 | 31229 84045 | 26776 19743 3157122 159.9 | 85.364 % | c | 144451 | 31194 83763 | 29421 22297 3752147 168.3 | 85.477 % | c | 148296 | 31194 83763 | 32363 26142 4561475 174.5 | 85.477 % | c | 154062 | 31107 83143 | 35500 31902 6012226 188.5 | 85.752 % | c | 162711 | 31084 82957 | 39021 40543 8025727 198.0 | 85.825 % | c | 175686 | 30879 81241 | 42641 19150 2911522 152.0 | 86.500 % | c | 195149 | 30746 80130 | 46703 38531 7468689 193.8 | 86.935 % | c | 224341 | 30702 79745 | 51299 25196 4714823 187.1 | 87.069 % | c | 268132 | 30467 77819 | 55998 19604 4016306 204.9 | 87.844 % | c | 333816 | 30240 75930 | 61138 32254 6508990 201.8 | 88.593 % | c c *** TERMINATED *** s SATISFIABLE v -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 C580 -C579 -C578 C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 C497 -C496 -C495 -C494 -C493 -C492 -C491 C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 C469 -C468 -C467 -C466 -C465 -C464 -C463 -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.77 0.92 0.89 2/53 13796 Raw data (stat): 13796 (runsolver) R 13795 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480400963 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0016 s] Raw data (loadavg): 0.81 0.92 0.89 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 3648 0 0 0 984 13 0 0 25 0 1 0 480400963 17813504 3626 4294967295 134512640 134672761 3221224560 3221222592 134566560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4349 3626 603 41 0 4308 0 vsize: 17396 [startup+20.003 s] Raw data (loadavg): 0.84 0.93 0.90 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 3667 0 0 0 1983 14 0 0 25 0 1 0 480400963 17956864 3645 4294967295 134512640 134672761 3221224560 3221222992 134604652 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4384 3645 603 41 0 4343 0 vsize: 17536 [startup+30.0037 s] Raw data (loadavg): 0.86 0.93 0.90 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 3698 0 0 0 2983 14 0 0 25 0 1 0 480400963 18153472 3676 4294967295 134512640 134672761 3221224560 3221223008 134643948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4432 3676 603 41 0 4391 0 vsize: 17728 [startup+40.0045 s] Raw data (loadavg): 0.88 0.93 0.90 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 4607 0 0 0 3980 17 0 0 25 0 1 0 480400963 19542016 4092 4294967295 134512640 134672761 3221224560 3221223104 134621086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4771 4092 603 41 0 4730 0 vsize: 19084 [startup+50.0051 s] Raw data (loadavg): 0.90 0.93 0.90 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 5368 0 0 0 4952 33 0 0 25 0 1 0 480400963 19582976 4125 4294967295 134512640 134672761 3221224560 3221222960 134604052 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4781 4125 603 41 0 4740 0 vsize: 19124 [startup+60.0061 s] Raw data (loadavg): 0.91 0.93 0.90 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 5368 0 0 0 5944 42 0 0 25 0 1 0 480400963 18714624 4015 4294967295 134512640 134672761 3221224560 3221223008 134643524 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4569 4015 603 41 0 4528 0 vsize: 18276 [startup+70.0068 s] Raw data (loadavg): 0.93 0.94 0.90 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 6957 0 0 0 6936 49 0 0 25 0 1 0 480400963 23461888 5140 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5728 5140 603 41 0 5687 0 vsize: 22912 [startup+80.0077 s] Raw data (loadavg): 0.94 0.94 0.90 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 6957 0 0 0 7934 51 0 0 25 0 1 0 480400963 23461888 5140 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5728 5140 603 41 0 5687 0 vsize: 22912 [startup+90.0086 s] Raw data (loadavg): 0.95 0.94 0.90 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 7947 0 0 0 8925 60 0 0 25 0 1 0 480400963 25444352 5676 4294967295 134512640 134672761 3221224560 3221223008 134643987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6212 5676 603 41 0 6171 0 vsize: 24848 [startup+100.009 s] Raw data (loadavg): 0.95 0.94 0.90 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 8147 0 0 0 9924 61 0 0 25 0 1 0 480400963 26230784 5876 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6404 5876 603 41 0 6363 0 vsize: 25616 [startup+110.01 s] Raw data (loadavg): 0.96 0.94 0.90 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 8965 0 0 0 10922 63 0 0 25 0 1 0 480400963 29515776 6694 4294967295 134512640 134672761 3221224560 3221223704 134616293 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7206 6694 603 41 0 7165 0 vsize: 28824 [startup+120.011 s] Raw data (loadavg): 0.97 0.94 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 9930 0 0 0 11921 65 0 0 25 0 1 0 480400963 33615872 7659 4294967295 134512640 134672761 3221224560 3221223704 134616139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8207 7659 603 41 0 8166 0 vsize: 32828 [startup+130.011 s] Raw data (loadavg): 0.97 0.95 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 10774 0 0 0 12920 66 0 0 25 0 1 0 480400963 37003264 8503 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9034 8503 603 41 0 8993 0 vsize: 36136 [startup+140.012 s] Raw data (loadavg): 0.98 0.95 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 11653 0 0 0 13918 68 0 0 25 0 1 0 480400963 40644608 9382 4294967295 134512640 134672761 3221224560 3221223704 134616350 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9923 9382 603 41 0 9882 0 vsize: 39692 [startup+150.013 s] Raw data (loadavg): 0.98 0.95 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 12726 0 0 0 14916 70 0 0 25 0 1 0 480400963 44949504 10455 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10974 10455 603 41 0 10933 0 vsize: 43896 [startup+160.014 s] Raw data (loadavg): 0.98 0.95 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 13520 0 0 0 15913 73 0 0 25 0 1 0 480400963 48209920 11249 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11770 11249 603 41 0 11729 0 vsize: 47080 [startup+170.015 s] Raw data (loadavg): 0.98 0.95 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 14228 0 0 0 16912 75 0 0 25 0 1 0 480400963 51200000 11957 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12500 11957 603 41 0 12459 0 vsize: 50000 [startup+180.015 s] Raw data (loadavg): 0.99 0.95 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 15147 0 0 0 17909 78 0 0 25 0 1 0 480400963 55042048 12876 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13438 12876 603 41 0 13397 0 vsize: 53752 [startup+190.016 s] Raw data (loadavg): 0.99 0.95 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 18898 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14422 13864 603 41 0 14381 0 vsize: 57688 [startup+200.017 s] Raw data (loadavg): 0.99 0.95 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 19898 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14422 13864 603 41 0 14381 0 vsize: 57688 [startup+210.018 s] Raw data (loadavg): 0.99 0.95 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 20898 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14422 13864 603 41 0 14381 0 vsize: 57688 [startup+220.018 s] Raw data (loadavg): 0.99 0.95 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 21898 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14422 13864 603 41 0 14381 0 vsize: 57688 [startup+230.019 s] Raw data (loadavg): 0.99 0.95 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 22899 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14422 13864 603 41 0 14381 0 vsize: 57688 [startup+240.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 23899 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14422 13864 603 41 0 14381 0 vsize: 57688 [startup+250.022 s] Raw data (loadavg): 0.99 0.96 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 24899 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14422 13864 603 41 0 14381 0 vsize: 57688 [startup+260.022 s] Raw data (loadavg): 0.99 0.96 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16637 0 0 0 25899 89 0 0 25 0 1 0 480400963 59072512 13864 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14422 13864 603 41 0 14381 0 vsize: 57688 [startup+270.023 s] Raw data (loadavg): 0.99 0.96 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16639 0 0 0 26899 89 0 0 25 0 1 0 480400963 59072512 13866 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14422 13866 603 41 0 14381 0 vsize: 57688 [startup+280.024 s] Raw data (loadavg): 0.99 0.96 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16642 0 0 0 27900 89 0 0 25 0 1 0 480400963 59072512 13869 4294967295 134512640 134672761 3221224560 3221223336 1075351081 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14422 13869 603 41 0 14381 0 vsize: 57688 [startup+290.025 s] Raw data (loadavg): 0.99 0.96 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16644 0 0 0 28900 89 0 0 25 0 1 0 480400963 59072512 13871 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14422 13871 603 41 0 14381 0 vsize: 57688 [startup+300.04 s] Raw data (loadavg): 0.99 0.96 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 16814 0 0 0 29901 89 0 0 25 0 1 0 480400963 59723776 14041 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14581 14041 603 41 0 14540 0 vsize: 58324 [startup+310.041 s] Raw data (loadavg): 0.99 0.96 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 17402 0 0 0 30900 91 0 0 25 0 1 0 480400963 62074880 14629 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15155 14629 603 41 0 15114 0 vsize: 60620 [startup+320.042 s] Raw data (loadavg): 0.99 0.96 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 17973 0 0 0 31899 92 0 0 25 0 1 0 480400963 64446464 15200 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15734 15200 603 41 0 15693 0 vsize: 62936 [startup+330.043 s] Raw data (loadavg): 0.99 0.96 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 18391 0 0 0 32898 93 0 0 25 0 1 0 480400963 66150400 15618 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16150 15618 603 41 0 16109 0 vsize: 64600 [startup+340.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19096 0 0 0 33897 95 0 0 25 0 1 0 480400963 68947968 16323 4294967295 134512640 134672761 3221224560 3221223008 134645372 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16833 16323 603 41 0 16792 0 vsize: 67332 [startup+350.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 34897 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16865 16336 603 41 0 16824 0 vsize: 67460 [startup+360.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 35897 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16865 16336 603 41 0 16824 0 vsize: 67460 [startup+370.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 36897 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223600 134612829 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16865 16336 603 41 0 16824 0 vsize: 67460 [startup+380.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 37898 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16865 16336 603 41 0 16824 0 vsize: 67460 [startup+390.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 38898 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16865 16336 603 41 0 16824 0 vsize: 67460 [startup+400.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 39898 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223600 134614207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16865 16336 603 41 0 16824 0 vsize: 67460 [startup+410.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 40898 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16865 16336 603 41 0 16824 0 vsize: 67460 [startup+420.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 41899 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16865 16336 603 41 0 16824 0 vsize: 67460 [startup+430.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 42899 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16865 16336 603 41 0 16824 0 vsize: 67460 [startup+440.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 43899 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16865 16336 603 41 0 16824 0 vsize: 67460 [startup+450.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 44899 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223744 134615711 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16865 16336 603 41 0 16824 0 vsize: 67460 [startup+460.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19132 0 0 0 45900 95 0 0 25 0 1 0 480400963 69079040 16336 4294967295 134512640 134672761 3221224560 3221223704 134616263 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16865 16336 603 41 0 16824 0 vsize: 67460 [startup+470.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19246 0 0 0 46899 95 0 0 25 0 1 0 480400963 69607424 16450 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16994 16450 603 41 0 16953 0 vsize: 67976 [startup+480.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19306 0 0 0 47900 95 0 0 25 0 1 0 480400963 69672960 16485 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17010 16485 603 41 0 16969 0 vsize: 68040 [startup+490.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19306 0 0 0 48900 95 0 0 25 0 1 0 480400963 69672960 16485 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17010 16485 603 41 0 16969 0 vsize: 68040 [startup+500.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 19306 0 0 0 49900 95 0 0 25 0 1 0 480400963 69672960 16485 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17010 16485 603 41 0 16969 0 vsize: 68040 [startup+510.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20390 0 0 0 50890 106 0 0 25 0 1 0 480400963 73072640 16799 4294967295 134512640 134672761 3221224560 3221223008 134643984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17840 16799 603 41 0 17799 0 vsize: 71360 [startup+520.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 51889 106 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+530.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 52889 106 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+540.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 53890 106 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+550.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 54890 106 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+560.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/53 13796 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 55890 106 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+570.064 s] Raw data (loadavg): 1.07 0.99 0.91 2/57 13839 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 56889 107 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+580.064 s] Raw data (loadavg): 1.06 0.99 0.91 2/53 13849 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 57889 107 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+590.065 s] Raw data (loadavg): 1.05 0.99 0.91 2/53 13849 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 58888 107 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223704 134616111 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+600.066 s] Raw data (loadavg): 1.04 0.99 0.91 2/53 13849 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 59888 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+610.066 s] Raw data (loadavg): 1.03 0.99 0.91 2/53 13849 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 60888 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+620.067 s] Raw data (loadavg): 1.03 0.99 0.91 2/53 13849 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 61888 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+630.068 s] Raw data (loadavg): 1.02 0.99 0.91 2/53 13849 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 62888 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223656 134616139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+640.068 s] Raw data (loadavg): 1.02 0.99 0.91 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 63888 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+650.069 s] Raw data (loadavg): 1.02 0.99 0.91 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 64889 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+660.07 s] Raw data (loadavg): 1.01 0.99 0.91 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 65889 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+670.072 s] Raw data (loadavg): 1.01 0.99 0.91 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 66889 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+680.072 s] Raw data (loadavg): 1.01 0.99 0.91 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 67890 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+690.072 s] Raw data (loadavg): 1.09 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 68890 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+700.073 s] Raw data (loadavg): 1.07 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 69890 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+710.074 s] Raw data (loadavg): 1.06 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 70890 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+720.075 s] Raw data (loadavg): 1.05 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 71890 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+730.076 s] Raw data (loadavg): 1.04 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 72891 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+740.076 s] Raw data (loadavg): 1.04 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20394 0 0 0 73891 108 0 0 25 0 1 0 480400963 73072640 16803 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17840 16803 603 41 0 17799 0 vsize: 71360 [startup+750.077 s] Raw data (loadavg): 1.03 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 20731 0 0 0 74890 108 0 0 25 0 1 0 480400963 74518528 17140 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18193 17140 603 41 0 18152 0 vsize: 72772 [startup+760.078 s] Raw data (loadavg): 1.02 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21156 0 0 0 75890 109 0 0 25 0 1 0 480400963 76226560 17565 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18610 17565 603 41 0 18569 0 vsize: 74440 [startup+770.079 s] Raw data (loadavg): 1.02 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 76889 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+780.08 s] Raw data (loadavg): 1.02 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 77890 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+790.081 s] Raw data (loadavg): 1.01 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 78890 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+800.082 s] Raw data (loadavg): 1.01 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 79890 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+810.083 s] Raw data (loadavg): 1.01 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 80890 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+820.083 s] Raw data (loadavg): 1.01 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 81891 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+830.084 s] Raw data (loadavg): 1.01 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 82891 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223704 134616156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+840.084 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 83891 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+850.086 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 84891 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+860.086 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 85892 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+870.087 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 86892 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+880.088 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 87892 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+890.088 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 21666 0 0 0 88892 110 0 0 25 0 1 0 480400963 78024704 18015 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19049 18015 603 41 0 19008 0 vsize: 76196 [startup+900.089 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 22063 0 0 0 89891 111 0 0 25 0 1 0 480400963 79724544 18412 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19464 18412 603 41 0 19423 0 vsize: 77856 [startup+910.09 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 22735 0 0 0 90890 113 0 0 25 0 1 0 480400963 82481152 19084 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20137 19084 603 41 0 20096 0 vsize: 80548 [startup+920.091 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23371 0 0 0 91889 114 0 0 25 0 1 0 480400963 85114880 19720 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20780 19720 603 41 0 20739 0 vsize: 83120 [startup+930.092 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13851 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 92888 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+940.093 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 93888 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+950.093 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 94888 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+960.099 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 95889 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+970.101 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 96889 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+980.101 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 97890 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+990.101 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 98890 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+1000.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 99890 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+1010.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 100890 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+1020.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 101891 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+1030.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 102891 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+1040.1 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 103891 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+1050.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 104891 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+1060.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 105892 115 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223744 134615635 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+1070.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 106892 116 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223600 134614280 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+1080.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 23814 0 0 0 107892 116 0 0 25 0 1 0 480400963 86790144 20098 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21189 20098 603 41 0 21148 0 vsize: 84756 [startup+1090.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24260 0 0 0 108891 117 0 0 25 0 1 0 480400963 88621056 20544 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21636 20544 603 41 0 21595 0 vsize: 86544 [startup+1100.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24634 0 0 0 109889 118 0 0 25 0 1 0 480400963 90202112 20918 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22022 20918 603 41 0 21981 0 vsize: 88088 [startup+1110.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 110889 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22177 21087 603 41 0 22136 0 vsize: 88708 [startup+1120.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 111889 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22177 21087 603 41 0 22136 0 vsize: 88708 [startup+1130.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 112890 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223664 134603768 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22177 21087 603 41 0 22136 0 vsize: 88708 [startup+1140.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 113890 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22177 21087 603 41 0 22136 0 vsize: 88708 [startup+1150.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 114890 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22177 21087 603 41 0 22136 0 vsize: 88708 [startup+1160.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 115890 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22177 21087 603 41 0 22136 0 vsize: 88708 [startup+1170.11 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 116891 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22177 21087 603 41 0 22136 0 vsize: 88708 [startup+1180.12 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24872 0 0 0 117891 119 0 0 25 0 1 0 480400963 90836992 21087 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22177 21087 603 41 0 22136 0 vsize: 88708 [startup+1190.12 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24873 0 0 0 118891 119 0 0 25 0 1 0 480400963 90836992 21088 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22177 21088 603 41 0 22136 0 vsize: 88708 [startup+1200.12 s] Raw data (loadavg): 1.00 1.00 0.92 2/53 13853 Raw data (stat): 13796 (minisat+) R 13795 7987 7986 0 -1 0 24873 0 0 0 119891 119 0 0 25 0 1 0 480400963 90836992 21088 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22177 21088 603 41 0 22136 0 vsize: 88708 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.19 s] Raw data (loadavg): 1.00 1.00 0.92 1/53 13853 Raw data (stat): 13796 (minisat+) Z 13795 7987 7986 0 -1 12 24874 0 0 0 119892 125 0 0 25 0 1 0 480400963 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.19 CPU time (s): 1200.18 CPU user time (s): 1198.92 CPU system time (s): 1.25681 CPU usage (%): 99.9992 Max. virtual memory (Kb): 88708 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####