Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0291.opb |
MD5SUM | 1d9168a9335e29df835d07b0bdf2adea |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 10447498 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 289 |
Biggest coefficient in the objective function | 80000000 |
Number of bits for the biggest coefficient in the objective function | 27 |
Sum of the numbers in the objective function | 686518451 |
Number of bits of the sum of numbers in the objective function | 30 |
Biggest number in a constraint | 80000000 |
Number of bits of the biggest number in a constraint | 27 |
Biggest sum of numbers in a constraint | 686518451 |
Number of bits of the biggest sum of numbers | 30 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.335948 |
Number of variables | 291 |
Total number of constraints | 543 |
Number of constraints which are clauses | 189 |
Number of constraints which are cardinality constraints (but not clauses) | 295 |
Number of constraints which are nor clauses,nor cardinality constraints | 59 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 53 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc4 THE 2005-04-21 09:08:41 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12154 boxname=wulflinc4 idbench=935 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1d9168a9335e29df835d07b0bdf2adea /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-p0291.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-p0291.opb /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-p0291.opb IDLAUNCH: 12154 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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: 380568 kB Buffers: 15612 kB Cached: 615564 kB SwapCached: 0 kB Active: 32680 kB Inactive: 601288 kB HighTotal: 131008 kB HighFree: 30156 kB LowTotal: 903652 kB LowFree: 350412 kB SwapTotal: 2097136 kB SwapFree: 2096992 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6816 kB Slab: 14428 kB Committed_AS: 71664 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 09:28:44 (client local time) WITH STATUS 10 IN 1200.29 SECONDS stats: 12154 7 1200.29 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 205 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .............................................................................................................................................................................................sssss c ---[ 144]---> BDD-cost: 3 c ---[ 139]---> BDD-cost: 3 c ---[ 14]---> BDD-cost: 1177 c ---[ 13]---> BDD-cost: 845 c ---[ 11]---> BDD-cost: 52 c ---[ 10]---> BDD-cost: 52 c ---[ 9]---> BDD-cost: 52 c ---[ 8]---> BDD-cost: 12 c ---[ 7]---> BDD-cost: 8 c ---[ 6]---> BDD-cost: 16 c ---[ 5]---> BDD-cost: 28 c ---[ 4]---> BDD-cost: 12 c ---[ 3]---> BDD-cost: 14 c ---[ 2]---> BDD-cost: 203 c ---[ 1]---> BDD-cost: 144 c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 6438 18748 | 2146 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 205610566[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:118485 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3 | 345759 810983 | 115253 3 14 4.7 | 0.000 % | c | 105 | 345605 810638 | 126778 90 3745 41.6 | 0.053 % | c | 257 | 345605 810638 | 139456 242 4405 18.2 | 0.053 % | c | 482 | 345521 810449 | 153401 466 5963 12.8 | 0.072 % | c | 819 | 345470 810334 | 168741 801 10036 12.5 | 0.084 % | c | 1326 | 345077 809448 | 185616 1300 26997 20.8 | 0.173 % | c ============================================================================== c [1mFound solution: 188210471[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 21 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1853 | 345424 811112 | 115141 1827 47761 26.1 | 0.173 % | c | 1954 | 345424 811112 | 126655 1928 48929 25.4 | 0.174 % | c | 2104 | 345344 810932 | 139320 2077 50614 24.4 | 0.192 % | c | 2329 | 345082 810339 | 153252 2293 63404 27.7 | 0.256 % | c | 2667 | 345082 810339 | 168577 2631 68864 26.2 | 0.256 % | c | 3173 | 344865 809850 | 185435 3133 72787 23.2 | 0.308 % | c | 3932 | 344812 809729 | 203979 3890 95012 24.4 | 0.322 % | c ============================================================================== c [1mFound solution: 146185330[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 23 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4265 | 345263 810880 | 115087 4222 107076 25.4 | 0.322 % | c ============================================================================== c [1mFound solution: 146185307[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 24 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4335 | 345177 810772 | 115059 4290 108180 25.2 | 0.322 % | c | 4435 | 345177 810772 | 126564 4390 114217 26.0 | 0.353 % | c ============================================================================== c [1mFound solution: 108859876[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 22 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4562 | 345206 810848 | 115068 4517 125721 27.8 | 0.353 % | c | 4662 | 345206 810848 | 126574 4617 126443 27.4 | 0.354 % | c | 4813 | 345206 810848 | 139232 4768 127286 26.7 | 0.354 % | c | 5040 | 345206 810848 | 153155 4995 134670 27.0 | 0.354 % | c | 5377 | 345206 810848 | 168471 5332 166177 31.2 | 0.354 % | c | 5885 | 345206 810848 | 185318 5840 181749 31.1 | 0.354 % | c | 6644 | 345145 810712 | 203849 6591 199356 30.2 | 0.368 % | c | 7785 | 345068 810540 | 224234 7724 250500 32.4 | 0.386 % | c | 9494 | 345068 810540 | 246658 9433 321015 34.0 | 0.386 % | c ============================================================================== c [1mFound solution: 106925952[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11853 | 345060 810552 | 115020 11778 432735 36.7 | 0.386 % | c | 11954 | 345060 810552 | 126522 11879 433846 36.5 | 0.432 % | c | 12104 | 345060 810552 | 139174 12029 435141 36.2 | 0.432 % | c | 12330 | 345060 810552 | 153091 12255 437802 35.7 | 0.432 % | c | 12667 | 345060 810552 | 168400 12592 452162 35.9 | 0.432 % | c ============================================================================== c [1mFound solution: 85083591[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 16 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13170 | 345079 810603 | 115026 13095 519296 39.7 | 0.432 % | c | 13271 | 344622 809567 | 126528 13174 521970 39.6 | 0.538 % | c | 13421 | 344622 809567 | 139181 13324 525178 39.4 | 0.538 % | c | 13648 | 344480 809245 | 153099 13547 526252 38.8 | 0.574 % | c | 13985 | 344480 809245 | 168409 13884 541214 39.0 | 0.574 % | c | 14491 | 344480 809245 | 185250 14390 595620 41.4 | 0.574 % | c | 15250 | 343815 807729 | 203775 15121 613759 40.6 | 0.737 % | c | 16391 | 343769 807626 | 224153 16260 657301 40.4 | 0.747 % | c | 18100 | 343710 807492 | 246568 17968 705751 39.3 | 0.761 % | c | 20662 | 343710 807492 | 271225 20530 741623 36.1 | 0.761 % | c ============================================================================== c [1mFound solution: 85076950[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21255 | 343946 808129 | 114648 21116 746090 35.3 | 0.761 % | c | 21355 | 343946 808129 | 126112 21216 752257 35.5 | 0.834 % | c | 21505 | 343946 808129 | 138724 21366 753045 35.2 | 0.834 % | c | 21730 | 343946 808129 | 152596 21591 754515 34.9 | 0.834 % | c | 22067 | 343885 807990 | 167856 21925 779075 35.5 | 0.849 % | c | 22573 | 343885 807990 | 184641 22431 815874 36.4 | 0.849 % | c ============================================================================== c [1mFound solution: 51875083[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:52778 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22993 | 483996 1135483 | 161332 22540 824610 36.6 | 0.849 % | c | 23094 | 483917 1135305 | 177465 22640 827755 36.6 | 1.801 % | c | 23244 | 483917 1135305 | 195211 22790 830876 36.5 | 1.801 % | c | 23471 | 483917 1135305 | 214732 23017 840506 36.5 | 1.801 % | c | 23808 | 483917 1135305 | 236206 23354 842629 36.1 | 1.801 % | c | 24315 | 483102 1133437 | 259826 23750 856772 36.1 | 1.953 % | c | 25074 | 483102 1133437 | 285809 24509 887149 36.2 | 1.953 % | c ============================================================================== c [1mFound solution: 51875003[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:84180 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25293 | 719985 1686385 | 239995 24726 892155 36.1 | 1.953 % | c | 25393 | 719985 1686385 | 263994 24826 896024 36.1 | 1.465 % | c | 25543 | 719837 1686051 | 290393 24974 915584 36.7 | 1.482 % | c | 25768 | 719307 1684869 | 319433 25193 918458 36.5 | 1.542 % | c | 26105 | 717743 1681299 | 351376 25412 930760 36.6 | 1.731 % | c ============================================================================== c [1mFound solution: 51553993[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 18 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26208 | 717978 1682432 | 239326 25475 934456 36.7 | 1.731 % | c | 26309 | 717693 1681785 | 263258 25571 935996 36.6 | 1.778 % | c | 26459 | 717546 1681452 | 289584 25717 936744 36.4 | 1.795 % | c | 26684 | 717530 1681416 | 318542 25936 940005 36.2 | 1.796 % | c | 27021 | 716549 1679189 | 350397 26242 941692 35.9 | 1.910 % | c | 27527 | 716408 1678871 | 385436 26743 962521 36.0 | 1.927 % | c | 28287 | 716408 1678871 | 423980 27503 982546 35.7 | 1.927 % | c ============================================================================== c [1mFound solution: 51472157[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 19 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 29242 | 716311 1678811 | 238770 28429 1045650 36.8 | 1.927 % | c | 29342 | 716281 1678743 | 262647 28525 1046711 36.7 | 2.005 % | c ============================================================================== c [1mFound solution: 50734660[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 19 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 29366 | 716374 1679102 | 238791 28549 1047371 36.7 | 2.005 % | c ============================================================================== c [1mFound solution: 50724062[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 17 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 29397 | 716388 1679156 | 238796 28580 1048585 36.7 | 2.005 % | c | 29497 | 716388 1679156 | 262675 28680 1049225 36.6 | 2.006 % | c | 29647 | 712828 1671026 | 288943 28771 1049935 36.5 | 2.422 % | c | 29872 | 712397 1670037 | 317837 28991 1055758 36.4 | 2.475 % | c | 30209 | 711346 1667626 | 349621 29155 1076015 36.9 | 2.606 % | c | 30715 | 711346 1667626 | 384583 29661 1111727 37.5 | 2.606 % | c ============================================================================== c [1mFound solution: 50550635[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 21 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30835 | 711358 1667667 | 237119 29781 1118170 37.5 | 2.606 % | c | 30935 | 711358 1667667 | 260830 29881 1124601 37.6 | 2.606 % | c | 31086 | 709417 1663202 | 286913 29878 1126051 37.7 | 2.848 % | c | 31312 | 709417 1663202 | 315605 30104 1133909 37.7 | 2.848 % | c ============================================================================== c [1mFound solution: 50550442[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 16 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31498 | 709430 1663240 | 236476 30290 1156462 38.2 | 2.848 % | c | 31600 | 709430 1663240 | 260123 30391 1160746 38.2 | 2.852 % | c ============================================================================== c [1mFound solution: 45379256[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:23266 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 31675 | 765272 1793710 | 255090 30323 1154339 38.1 | 2.852 % | c | 31775 | 765272 1793710 | 280599 30423 1155803 38.0 | 3.477 % | c | 31925 | 765272 1793710 | 308658 30573 1160513 38.0 | 3.477 % | c | 32152 | 763211 1789011 | 339524 30745 1162558 37.8 | 3.705 % | c | 32489 | 763211 1789011 | 373477 31082 1206559 38.8 | 3.705 % | c | 32997 | 763211 1789011 | 410824 31590 1234463 39.1 | 3.705 % | c ============================================================================== c [1mFound solution: 44222971[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:78899 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 33531 | 980489 2296150 | 326829 31882 1224198 38.4 | 3.705 % | c | 33631 | 978465 2291563 | 359511 31885 1221354 38.3 | 3.628 % | c | 33781 | 800145 1880269 | 395463 26247 869217 33.1 | 19.914 % | c ============================================================================== c [1mFound solution: 28913802[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:85693 Base: 2 5 2 2 2 2 2 2 3 3 3 3 2 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 33918 | 1013010 2377890 | 337670 25098 795849 31.7 | 19.914 % | c | 34018 | 1012919 2377678 | 371437 25197 796428 31.6 | 18.299 % | c | 34169 | 1012919 2377678 | 408580 25348 813578 32.1 | 18.299 % | c | 34394 | 1012173 2375961 | 449438 25566 820041 32.1 | 18.355 % | c ============================================================================== c [1mFound solution: 25746408[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:54578 Base: 2 5 2 2 2 2 2 2 3 3 3 3 2 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34521 | 1164173 2731215 | 388057 25693 827573 32.2 | 18.355 % | c | 34621 | 1164173 2731215 | 426862 25793 828997 32.1 | 16.377 % | c | 34771 | 1164060 2730960 | 469548 25939 833010 32.1 | 16.383 % | c | 34996 | 1164060 2730960 | 516503 26164 860805 32.9 | 16.383 % | c | 35334 | 1164060 2730960 | 568154 26502 891785 33.6 | 16.383 % | c | 35840 | 1164060 2730960 | 624969 27008 901110 33.4 | 16.383 % | c | 36599 | 1162439 2727228 | 687466 27652 909409 32.9 | 16.485 % | c ============================================================================== c [1mFound solution: 25678207[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 18 Base: 2 5 2 2 2 2 2 2 3 3 3 3 2 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 37494 | 1163000 2729107 | 387666 28544 939199 32.9 | 16.485 % | c | 37595 | 1163000 2729107 | 426432 28645 940262 32.8 | 16.478 % | c | 37745 | 1162926 2728941 | 469075 28794 941027 32.7 | 16.482 % | c ============================================================================== c [1mFound solution: 25107592[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 18 Base: 2 5 2 2 2 2 2 2 3 3 3 3 2 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 37809 | 1162582 2728324 | 387527 28854 944060 32.7 | 16.482 % | #### 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.97 0.94 2/54 5028 Raw data (stat): 5028 (runsolver) R 5027 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485656577 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0003 s] Raw data (loadavg): 0.87 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 505 0 0 0 997 1 0 0 25 0 1 0 485656577 3727360 483 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 910 483 603 41 0 869 0 vsize: 3640 [startup+20.001 s] Raw data (loadavg): 0.89 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 505 0 0 0 1997 1 0 0 25 0 1 0 485656577 3727360 483 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 910 483 603 41 0 869 0 vsize: 3640 [startup+30.0006 s] Raw data (loadavg): 0.91 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 505 0 0 0 2997 1 0 0 25 0 1 0 485656577 3727360 483 4294967295 134512640 134672761 3221224544 3221222496 134522369 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 910 483 603 41 0 869 0 vsize: 3640 [startup+40.0008 s] Raw data (loadavg): 0.92 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 505 0 0 0 3996 2 0 0 25 0 1 0 485656577 3727360 483 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 910 483 603 41 0 869 0 vsize: 3640 [startup+50.002 s] Raw data (loadavg): 0.93 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 9944 0 0 0 4972 26 0 0 25 0 1 0 485656577 42864640 9607 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10465 9607 603 41 0 10424 0 vsize: 41860 [startup+60.0013 s] Raw data (loadavg): 0.94 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10126 0 0 0 5971 27 0 0 25 0 1 0 485656577 43663360 9789 4294967295 134512640 134672761 3221224544 3221221232 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10660 9789 603 41 0 10619 0 vsize: 42640 [startup+70.0024 s] Raw data (loadavg): 0.95 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10126 0 0 0 6972 27 0 0 25 0 1 0 485656577 43663360 9789 4294967295 134512640 134672761 3221224544 3221221952 134597193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10660 9789 603 41 0 10619 0 vsize: 42640 [startup+80.0032 s] Raw data (loadavg): 0.96 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10126 0 0 0 7971 27 0 0 25 0 1 0 485656577 43663360 9789 4294967295 134512640 134672761 3221224544 3221222672 134597262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10660 9789 603 41 0 10619 0 vsize: 42640 [startup+90.0038 s] Raw data (loadavg): 0.96 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10126 0 0 0 8971 28 0 0 25 0 1 0 485656577 43663360 9789 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10660 9789 603 41 0 10619 0 vsize: 42640 [startup+100.004 s] Raw data (loadavg): 0.97 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10126 0 0 0 9971 28 0 0 25 0 1 0 485656577 43663360 9789 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10660 9789 603 41 0 10619 0 vsize: 42640 [startup+110.004 s] Raw data (loadavg): 0.97 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10161 0 0 0 10970 29 0 0 25 0 1 0 485656577 43905024 9823 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10719 9823 603 41 0 10678 0 vsize: 42876 [startup+120.005 s] Raw data (loadavg): 0.98 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10228 0 0 0 11970 29 0 0 25 0 1 0 485656577 44232704 9890 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10799 9890 603 41 0 10758 0 vsize: 43196 [startup+130.005 s] Raw data (loadavg): 0.98 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10228 0 0 0 12970 29 0 0 25 0 1 0 485656577 44232704 9890 4294967295 134512640 134672761 3221224544 3221221376 134597165 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10799 9890 603 41 0 10758 0 vsize: 43196 [startup+140.005 s] Raw data (loadavg): 0.98 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10228 0 0 0 13969 30 0 0 25 0 1 0 485656577 44232704 9890 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10799 9890 603 41 0 10758 0 vsize: 43196 [startup+150.006 s] Raw data (loadavg): 0.98 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10228 0 0 0 14969 30 0 0 25 0 1 0 485656577 44232704 9890 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10799 9890 603 41 0 10758 0 vsize: 43196 [startup+160.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10228 0 0 0 15969 31 0 0 25 0 1 0 485656577 44232704 9890 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10799 9890 603 41 0 10758 0 vsize: 43196 [startup+170.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10252 0 0 0 16969 31 0 0 25 0 1 0 485656577 44232704 9914 4294967295 134512640 134672761 3221224544 3221222208 134522369 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10799 9914 603 41 0 10758 0 vsize: 43196 [startup+180.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10252 0 0 0 17968 31 0 0 25 0 1 0 485656577 44232704 9914 4294967295 134512640 134672761 3221224544 3221221656 134597415 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10799 9914 603 41 0 10758 0 vsize: 43196 [startup+190.006 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10252 0 0 0 18969 31 0 0 25 0 1 0 485656577 44232704 9914 4294967295 134512640 134672761 3221224544 3221222384 134597215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10799 9914 603 41 0 10758 0 vsize: 43196 [startup+200.007 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10252 0 0 0 19969 31 0 0 25 0 1 0 485656577 44232704 9914 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10799 9914 603 41 0 10758 0 vsize: 43196 [startup+210.007 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10265 0 0 0 20969 31 0 0 25 0 1 0 485656577 44232704 9924 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10799 9924 603 41 0 10758 0 vsize: 43196 [startup+220.007 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10266 0 0 0 21969 31 0 0 25 0 1 0 485656577 44232704 9925 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10799 9925 603 41 0 10758 0 vsize: 43196 [startup+230.007 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10266 0 0 0 22969 31 0 0 25 0 1 0 485656577 44232704 9925 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10799 9925 603 41 0 10758 0 vsize: 43196 [startup+240.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10266 0 0 0 23969 31 0 0 25 0 1 0 485656577 44232704 9925 4294967295 134512640 134672761 3221224544 3221222240 134597203 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10799 9925 603 41 0 10758 0 vsize: 43196 [startup+250.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10266 0 0 0 24970 31 0 0 25 0 1 0 485656577 44232704 9925 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10799 9925 603 41 0 10758 0 vsize: 43196 [startup+260.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10290 0 0 0 25970 31 0 0 25 0 1 0 485656577 44343296 9949 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10826 9949 603 41 0 10785 0 vsize: 43304 [startup+270.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10338 0 0 0 26970 31 0 0 25 0 1 0 485656577 44605440 9997 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10890 9997 603 41 0 10849 0 vsize: 43560 [startup+280.008 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10376 0 0 0 27970 31 0 0 25 0 1 0 485656577 44740608 10035 4294967295 134512640 134672761 3221224544 3221223648 134560160 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10923 10035 603 41 0 10882 0 vsize: 43692 [startup+290.01 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10469 0 0 0 28970 32 0 0 25 0 1 0 485656577 45146112 10128 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11022 10128 603 41 0 10981 0 vsize: 44088 [startup+300.01 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10572 0 0 0 29969 33 0 0 25 0 1 0 485656577 45551616 10231 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11121 10231 603 41 0 11080 0 vsize: 44484 [startup+310.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10614 0 0 0 30969 33 0 0 25 0 1 0 485656577 45686784 10273 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11154 10273 603 41 0 11113 0 vsize: 44616 [startup+320.009 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10614 0 0 0 31969 33 0 0 25 0 1 0 485656577 45686784 10273 4294967295 134512640 134672761 3221224544 3221222528 134597176 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11154 10273 603 41 0 11113 0 vsize: 44616 [startup+330.01 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10614 0 0 0 32970 33 0 0 25 0 1 0 485656577 45686784 10273 4294967295 134512640 134672761 3221224544 3221222240 134597191 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11154 10273 603 41 0 11113 0 vsize: 44616 [startup+340.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10614 0 0 0 33970 33 0 0 25 0 1 0 485656577 45686784 10273 4294967295 134512640 134672761 3221224544 3221221808 134597012 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11154 10273 603 41 0 11113 0 vsize: 44616 [startup+350.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10647 0 0 0 34970 33 0 0 25 0 1 0 485656577 45891584 10303 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11204 10303 603 41 0 11163 0 vsize: 44816 [startup+360.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10714 0 0 0 35970 33 0 0 25 0 1 0 485656577 46157824 10370 4294967295 134512640 134672761 3221224544 3221221520 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11269 10370 603 41 0 11228 0 vsize: 45076 [startup+370.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10714 0 0 0 36970 33 0 0 25 0 1 0 485656577 46157824 10370 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11269 10370 603 41 0 11228 0 vsize: 45076 [startup+380.011 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10714 0 0 0 37970 33 0 0 25 0 1 0 485656577 46157824 10370 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11269 10370 603 41 0 11228 0 vsize: 45076 [startup+390.012 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10714 0 0 0 38970 33 0 0 25 0 1 0 485656577 46157824 10370 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11269 10370 603 41 0 11228 0 vsize: 45076 [startup+400.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10741 0 0 0 39970 33 0 0 25 0 1 0 485656577 46157824 10396 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11269 10396 603 41 0 11228 0 vsize: 45076 [startup+410.013 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10788 0 0 0 40970 33 0 0 25 0 1 0 485656577 46428160 10443 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11335 10443 603 41 0 11294 0 vsize: 45340 [startup+420.014 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10888 0 0 0 41970 34 0 0 25 0 1 0 485656577 46899200 10543 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11450 10543 603 41 0 11409 0 vsize: 45800 [startup+430.014 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10987 0 0 0 42970 34 0 0 25 0 1 0 485656577 47296512 10642 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11547 10642 603 41 0 11506 0 vsize: 46188 [startup+440.015 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10987 0 0 0 43971 34 0 0 25 0 1 0 485656577 47296512 10642 4294967295 134512640 134672761 3221224544 3221221632 134522373 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11547 10642 603 41 0 11506 0 vsize: 46188 [startup+450.014 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10987 0 0 0 44971 34 0 0 25 0 1 0 485656577 47296512 10642 4294967295 134512640 134672761 3221224544 3221221952 134597008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11547 10642 603 41 0 11506 0 vsize: 46188 [startup+460.014 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10987 0 0 0 45971 34 0 0 25 0 1 0 485656577 47296512 10642 4294967295 134512640 134672761 3221224544 3221223104 134597195 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11547 10642 603 41 0 11506 0 vsize: 46188 [startup+470.015 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 10987 0 0 0 46971 34 0 0 25 0 1 0 485656577 47296512 10642 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11547 10642 603 41 0 11506 0 vsize: 46188 [startup+480.015 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 11058 0 0 0 47971 34 0 0 25 0 1 0 485656577 47562752 10709 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11612 10709 603 41 0 11571 0 vsize: 46448 [startup+490.016 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 11103 0 0 0 48971 34 0 0 25 0 1 0 485656577 47693824 10754 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11644 10754 603 41 0 11603 0 vsize: 46576 [startup+500.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 11103 0 0 0 49971 34 0 0 25 0 1 0 485656577 47693824 10754 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11644 10754 603 41 0 11603 0 vsize: 46576 [startup+510.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 11103 0 0 0 50972 34 0 0 25 0 1 0 485656577 47693824 10754 4294967295 134512640 134672761 3221224544 3221222148 1074971756 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11644 10754 603 41 0 11603 0 vsize: 46576 [startup+520.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 11103 0 0 0 51972 34 0 0 25 0 1 0 485656577 47693824 10754 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11644 10754 603 41 0 11603 0 vsize: 46576 [startup+530.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 15507 0 0 0 52962 44 0 0 25 0 1 0 485656577 70733824 14828 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17269 14828 603 41 0 17228 0 vsize: 69076 [startup+540.019 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 15524 0 0 0 53962 44 0 0 25 0 1 0 485656577 70733824 14845 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17269 14845 603 41 0 17228 0 vsize: 69076 [startup+550.019 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 15679 0 0 0 54962 44 0 0 25 0 1 0 485656577 71659520 15000 4294967295 134512640 134672761 3221224544 3221221520 134597225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17495 15000 603 41 0 17454 0 vsize: 69980 [startup+560.019 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 15679 0 0 0 55962 44 0 0 25 0 1 0 485656577 71659520 15000 4294967295 134512640 134672761 3221224544 3221221520 134597185 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17495 15000 603 41 0 17454 0 vsize: 69980 [startup+570.02 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 15679 0 0 0 56963 44 0 0 25 0 1 0 485656577 71659520 15000 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17495 15000 603 41 0 17454 0 vsize: 69980 [startup+580.019 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 15679 0 0 0 57963 44 0 0 25 0 1 0 485656577 71659520 15000 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17495 15000 603 41 0 17454 0 vsize: 69980 [startup+590.02 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21724 0 0 0 58950 57 0 0 25 0 1 0 485656577 91209728 21045 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22268 21045 603 41 0 22227 0 vsize: 89072 [startup+600.021 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21782 0 0 0 59950 57 0 0 25 0 1 0 485656577 91344896 21103 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22301 21103 603 41 0 22260 0 vsize: 89204 [startup+610.021 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21952 0 0 0 60950 58 0 0 25 0 1 0 485656577 91480064 21273 4294967295 134512640 134672761 3221224544 3221221952 134597256 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22334 21273 603 41 0 22293 0 vsize: 89336 [startup+620.021 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21952 0 0 0 61950 58 0 0 25 0 1 0 485656577 91480064 21273 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22334 21273 603 41 0 22293 0 vsize: 89336 [startup+630.021 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21952 0 0 0 62950 58 0 0 25 0 1 0 485656577 91480064 21273 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22334 21273 603 41 0 22293 0 vsize: 89336 [startup+640.022 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21952 0 0 0 63951 58 0 0 25 0 1 0 485656577 91480064 21273 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22334 21273 603 41 0 22293 0 vsize: 89336 [startup+650.022 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 21980 0 0 0 64951 58 0 0 25 0 1 0 485656577 91488256 21298 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22336 21298 603 41 0 22295 0 vsize: 89344 [startup+660.022 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22037 0 0 0 65951 58 0 0 25 0 1 0 485656577 91750400 21355 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22400 21355 603 41 0 22359 0 vsize: 89600 [startup+670.022 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22060 0 0 0 66951 58 0 0 25 0 1 0 485656577 91885568 21378 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22433 21378 603 41 0 22392 0 vsize: 89732 [startup+680.022 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22106 0 0 0 67951 58 0 0 25 0 1 0 485656577 92155904 21424 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22499 21424 603 41 0 22458 0 vsize: 89996 [startup+690.023 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22106 0 0 0 68951 58 0 0 25 0 1 0 485656577 92155904 21424 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22499 21424 603 41 0 22458 0 vsize: 89996 [startup+700.023 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22106 0 0 0 69951 58 0 0 25 0 1 0 485656577 92155904 21424 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22499 21424 603 41 0 22458 0 vsize: 89996 [startup+710.023 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22106 0 0 0 70952 58 0 0 25 0 1 0 485656577 92155904 21424 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22499 21424 603 41 0 22458 0 vsize: 89996 [startup+720.024 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22141 0 0 0 71952 58 0 0 25 0 1 0 485656577 92139520 21459 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22495 21459 603 41 0 22454 0 vsize: 89980 [startup+730.024 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22141 0 0 0 72952 58 0 0 25 0 1 0 485656577 92139520 21459 4294967295 134512640 134672761 3221224544 3221221548 1075346551 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22495 21459 603 41 0 22454 0 vsize: 89980 [startup+740.026 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22141 0 0 0 73952 58 0 0 25 0 1 0 485656577 92139520 21459 4294967295 134512640 134672761 3221224544 3221221952 134597161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22495 21459 603 41 0 22454 0 vsize: 89980 [startup+750.026 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22141 0 0 0 74953 58 0 0 25 0 1 0 485656577 92139520 21459 4294967295 134512640 134672761 3221224544 3221222384 134597018 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22495 21459 603 41 0 22454 0 vsize: 89980 [startup+760.026 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22153 0 0 0 75953 58 0 0 25 0 1 0 485656577 92168192 21468 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22502 21468 603 41 0 22461 0 vsize: 90008 [startup+770.027 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22153 0 0 0 76953 58 0 0 25 0 1 0 485656577 92168192 21468 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22502 21468 603 41 0 22461 0 vsize: 90008 [startup+780.028 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22153 0 0 0 77953 58 0 0 25 0 1 0 485656577 92168192 21468 4294967295 134512640 134672761 3221224544 3221221808 134597184 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22502 21468 603 41 0 22461 0 vsize: 90008 [startup+790.029 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22153 0 0 0 78953 58 0 0 25 0 1 0 485656577 92168192 21468 4294967295 134512640 134672761 3221224544 3221221952 134597195 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22502 21468 603 41 0 22461 0 vsize: 90008 [startup+800.029 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22162 0 0 0 79953 58 0 0 25 0 1 0 485656577 92192768 21474 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22508 21474 603 41 0 22467 0 vsize: 90032 [startup+810.028 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22162 0 0 0 80954 58 0 0 25 0 1 0 485656577 92192768 21474 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22508 21474 603 41 0 22467 0 vsize: 90032 [startup+820.03 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22184 0 0 0 81954 58 0 0 25 0 1 0 485656577 92327936 21496 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22541 21496 603 41 0 22500 0 vsize: 90164 [startup+830.029 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22212 0 0 0 82954 58 0 0 25 0 1 0 485656577 92450816 21524 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22571 21524 603 41 0 22530 0 vsize: 90284 [startup+840.03 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22212 0 0 0 83954 58 0 0 25 0 1 0 485656577 92450816 21524 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22571 21524 603 41 0 22530 0 vsize: 90284 [startup+850.031 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22212 0 0 0 84954 58 0 0 25 0 1 0 485656577 92450816 21524 4294967295 134512640 134672761 3221224544 3221221808 134597203 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22571 21524 603 41 0 22530 0 vsize: 90284 [startup+860.031 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22212 0 0 0 85954 58 0 0 25 0 1 0 485656577 92450816 21524 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22571 21524 603 41 0 22530 0 vsize: 90284 [startup+870.032 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22239 0 0 0 86954 58 0 0 25 0 1 0 485656577 92499968 21550 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22583 21550 603 41 0 22542 0 vsize: 90332 [startup+880.032 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22253 0 0 0 87955 58 0 0 25 0 1 0 485656577 92635136 21564 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22616 21564 603 41 0 22575 0 vsize: 90464 [startup+890.033 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22253 0 0 0 88955 58 0 0 25 0 1 0 485656577 92635136 21564 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22616 21564 603 41 0 22575 0 vsize: 90464 [startup+900.033 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22253 0 0 0 89955 58 0 0 25 0 1 0 485656577 92635136 21564 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22616 21564 603 41 0 22575 0 vsize: 90464 [startup+910.032 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22253 0 0 0 90955 58 0 0 25 0 1 0 485656577 92635136 21564 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22616 21564 603 41 0 22575 0 vsize: 90464 [startup+920.033 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22280 0 0 0 91955 58 0 0 25 0 1 0 485656577 92655616 21588 4294967295 134512640 134672761 3221224544 3221223808 134562470 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22621 21588 603 41 0 22580 0 vsize: 90484 [startup+930.033 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22281 0 0 0 92955 58 0 0 25 0 1 0 485656577 92655616 21589 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22621 21589 603 41 0 22580 0 vsize: 90484 [startup+940.034 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22281 0 0 0 93956 58 0 0 25 0 1 0 485656577 92655616 21589 4294967295 134512640 134672761 3221224544 3221222096 134597184 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22621 21589 603 41 0 22580 0 vsize: 90484 [startup+950.039 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22281 0 0 0 94956 58 0 0 25 0 1 0 485656577 92655616 21589 4294967295 134512640 134672761 3221224544 3221222384 134597176 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22621 21589 603 41 0 22580 0 vsize: 90484 [startup+960.045 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 22281 0 0 0 95957 58 0 0 25 0 1 0 485656577 92655616 21589 4294967295 134512640 134672761 3221224544 3221222496 134522369 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22621 21589 603 41 0 22580 0 vsize: 90484 [startup+970.045 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23850 0 0 0 96953 63 0 0 25 0 1 0 485656577 117944320 23158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28795 23158 603 41 0 28754 0 vsize: 115180 [startup+980.045 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23866 0 0 0 97953 63 0 0 25 0 1 0 485656577 117944320 23174 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28795 23174 603 41 0 28754 0 vsize: 115180 [startup+990.046 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23902 0 0 0 98953 63 0 0 25 0 1 0 485656577 118075392 23210 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28827 23210 603 41 0 28786 0 vsize: 115308 [startup+1000.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23945 0 0 0 99953 63 0 0 25 0 1 0 485656577 118214656 23253 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28861 23253 603 41 0 28820 0 vsize: 115444 [startup+1010.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23971 0 0 0 100953 63 0 0 25 0 1 0 485656577 118214656 23279 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28861 23279 603 41 0 28820 0 vsize: 115444 [startup+1020.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23971 0 0 0 101954 63 0 0 25 0 1 0 485656577 118214656 23279 4294967295 134512640 134672761 3221224544 3221222816 134597176 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28861 23279 603 41 0 28820 0 vsize: 115444 [startup+1030.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23971 0 0 0 102954 63 0 0 25 0 1 0 485656577 118214656 23279 4294967295 134512640 134672761 3221224544 3221222352 134522369 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28861 23279 603 41 0 28820 0 vsize: 115444 [startup+1040.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 23971 0 0 0 103954 63 0 0 25 0 1 0 485656577 118214656 23279 4294967295 134512640 134672761 3221224544 3221222784 134522369 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28861 23279 603 41 0 28820 0 vsize: 115444 [startup+1050.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 30994 0 0 0 104940 78 0 0 25 0 1 0 485656577 138240000 29643 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33750 29643 603 41 0 33709 0 vsize: 135000 [startup+1060.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 31071 0 0 0 105940 78 0 0 25 0 1 0 485656577 139563008 29720 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34073 29720 603 41 0 34032 0 vsize: 136292 [startup+1070.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 31071 0 0 0 106940 78 0 0 25 0 1 0 485656577 139563008 29720 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34073 29720 603 41 0 34032 0 vsize: 136292 [startup+1080.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 35907 0 0 0 107929 89 0 0 25 0 1 0 485656577 152698880 34556 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37280 34556 603 41 0 37239 0 vsize: 149120 [startup+1090.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 35981 0 0 0 108929 89 0 0 25 0 1 0 485656577 152698880 34630 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37280 34630 603 41 0 37239 0 vsize: 149120 [startup+1100.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 36067 0 0 0 109929 90 0 0 25 0 1 0 485656577 152698880 34716 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37280 34716 603 41 0 37239 0 vsize: 149120 [startup+1110.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 39755 0 0 0 110922 97 0 0 25 0 1 0 485656577 167436288 38404 4294967295 134512640 134672761 3221224544 3221219584 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 40878 38405 603 41 0 40837 0 vsize: 163512 [startup+1120.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 39799 0 0 0 111922 97 0 0 25 0 1 0 485656577 167706624 38448 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 40944 38448 603 41 0 40903 0 vsize: 163776 [startup+1130.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 39843 0 0 0 112922 97 0 0 25 0 1 0 485656577 167841792 38492 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 40977 38492 603 41 0 40936 0 vsize: 163908 [startup+1140.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 39895 0 0 0 113922 97 0 0 25 0 1 0 485656577 167976960 38544 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41010 38544 603 41 0 40969 0 vsize: 164040 [startup+1150.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 39997 0 0 0 114922 97 0 0 25 0 1 0 485656577 168124416 38646 4294967295 134512640 134672761 3221224544 3221221868 1075349761 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41046 38646 603 41 0 41005 0 vsize: 164184 [startup+1160.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 39997 0 0 0 115922 97 0 0 25 0 1 0 485656577 168124416 38646 4294967295 134512640 134672761 3221224544 3221222240 134597184 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41046 38646 603 41 0 41005 0 vsize: 164184 [startup+1170.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 40026 0 0 0 116922 98 0 0 25 0 1 0 485656577 168124416 38675 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41046 38675 603 41 0 41005 0 vsize: 164184 [startup+1180.05 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 40026 0 0 0 117922 98 0 0 25 0 1 0 485656577 168124416 38675 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41046 38675 603 41 0 41005 0 vsize: 164184 [startup+1190.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 40041 0 0 0 118923 98 0 0 25 0 1 0 485656577 168198144 38690 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41064 38690 603 41 0 41023 0 vsize: 164256 [startup+1200.06 s] Raw data (loadavg): 0.99 0.97 0.94 2/54 5028 Raw data (stat): 5028 (minisat+) R 5027 5897 5896 0 -1 0 40041 0 0 0 119923 98 0 0 25 0 1 0 485656577 168198144 38690 4294967295 134512640 134672761 3221224544 3221222228 134597471 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41064 38690 603 41 0 41023 0 vsize: 164256 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.13 s] Raw data (loadavg): 0.99 0.97 0.94 1/54 5028 Raw data (stat): 5028 (minisat+) Z 5027 5897 5896 0 -1 12 40044 0 0 0 119923 105 0 0 25 0 1 0 485656577 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.13 CPU time (s): 1200.29 CPU user time (s): 1199.23 CPU system time (s): 1.05584 CPU usage (%): 100.013 Max. virtual memory (Kb): 164256 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####