Name | normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cm42a.opb |
MD5SUM | 62b75258091a8b1382fa8b1c633d9511 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 694 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 99 |
Biggest coefficient in the objective function | 60 |
Number of bits for the biggest coefficient in the objective function | 6 |
Sum of the numbers in the objective function | 4087 |
Number of bits of the sum of numbers in the objective function | 12 |
Biggest number in a constraint | 60 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 4087 |
Number of bits of the biggest sum of numbers | 12 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.168973 |
Number of variables | 99 |
Total number of constraints | 185 |
Number of constraints which are clauses | 185 |
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 | 20 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc2 THE 2005-04-14 00:37:36 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4012 boxname=wulflinc2 idbench=252 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 62b75258091a8b1382fa8b1c633d9511 /oldhome/oroussel/tmp/wulflinc2/normalized-cm42a.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc2/normalized-cm42a.opb /oldhome/oroussel/tmp/wulflinc2/normalized-cm42a.opb IDLAUNCH: 4012 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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: 902392 kB Buffers: 34752 kB Cached: 76968 kB SwapCached: 4 kB Active: 56484 kB Inactive: 58060 kB HighTotal: 131008 kB HighFree: 50260 kB LowTotal: 903652 kB LowFree: 852132 kB SwapTotal: 2097136 kB SwapFree: 2097132 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6916 kB Slab: 12048 kB Committed_AS: 71676 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 00:57:38 (client local time) WITH STATUS 10 IN 1200.35 SECONDS stats: 4012 7 1200.35 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 185 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 | 185 626 | 55 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 85/85 c | 0 | 185 626 | 74 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 0.013997 s) c ============================================================================== c [1mFound solution: 939[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8480 Base: 3 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 21020 49263 | 6305 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/7707 c -- var.elim.: 2000/7707 c -- var.elim.: 3000/7707 c -- var.elim.: 4000/7707 c -- var.elim.: 5000/7707 c -- var.elim.: 6000/7707 c -- var.elim.: 7000/7707 c -- var.elim.: 7707/7707 c -- var.elim.: 1000/4213 c -- var.elim.: 2000/4213 c -- var.elim.: 3000/4213 c -- var.elim.: 4000/4213 c -- var.elim.: 4213/4213 c -- subsuming c -- var.elim.: 880/880 c -- var.elim.: 260/260 c -- subsuming c -- var.elim.: 6/6 c | 0 | 18633 59861 | -- 0 -- -- | -- | -2387/10599 c | 0 | 18633 59861 | 7453 0 0 nan | 0.000 % | c | 101 | 18633 59861 | 8198 101 1565 15.5 | 0.024 % | c | 252 | 18633 59861 | 9018 252 3697 14.7 | 0.024 % | c | 477 | 18201 58148 | 9690 470 14358 30.5 | 1.689 % | c | 814 | 17983 57167 | 10531 728 17384 23.9 | 2.307 % | c | 1321 | 17983 57167 | 11584 1235 51265 41.5 | 2.307 % | c | 2080 | 17983 57167 | 12743 1994 61630 30.9 | 2.307 % | c | 3219 | 17983 57167 | 14017 3133 117087 37.4 | 2.307 % | c ============================================================================== c (current CPU-time: 4.5903 s) c ============================================================================== c [1mFound solution: 866[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6777 Base: 3 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 3408 | 34827 96642 | 10448 3322 129356 38.9 | 2.307 % | c -- subsuming c -- var.elim.: 1000/7350 c -- var.elim.: 2000/7350 c -- var.elim.: 3000/7350 c -- var.elim.: 4000/7350 c -- var.elim.: 5000/7350 c -- var.elim.: 6000/7350 c -- var.elim.: 7000/7350 c -- var.elim.: 7350/7350 c -- var.elim.: 1000/4089 c -- var.elim.: 2000/4089 c -- var.elim.: 3000/4089 c -- var.elim.: 4000/4089 c -- var.elim.: 4089/4089 c -- var.elim.: 314/314 c -- var.elim.: 274/274 c -- subsuming c -- var.elim.: 956/956 c -- var.elim.: 35/35 c | 3408 | 32588 105396 | -- 3322 -- -- | -- | -2239/8755 c | 3408 | 32588 105396 | 13035 3147 106030 33.7 | 2.307 % | c | 3508 | 32588 105396 | 14338 3247 109693 33.8 | 1.334 % | c | 3659 | 32588 105396 | 15772 3398 120859 35.6 | 1.334 % | c | 3884 | 32588 105396 | 17349 3623 131110 36.2 | 1.334 % | c | 4222 | 32588 105396 | 19084 3961 148623 37.5 | 1.334 % | c | 4728 | 32588 105396 | 20993 4467 167381 37.5 | 1.334 % | c | 5487 | 32588 105396 | 23092 5226 203929 39.0 | 1.334 % | c | 6628 | 32588 105396 | 25401 6367 309182 48.6 | 1.334 % | c ============================================================================== c (current CPU-time: 14.8707 s) c ============================================================================== c [1mFound solution: 865[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 7916 | 33186 107060 | 9955 7655 425161 55.5 | 1.334 % | c -- subsuming c -- var.elim.: 963/963 c -- var.elim.: 541/541 c -- subsuming c -- var.elim.: 336/336 c | 7916 | 32788 107150 | -- 7655 -- -- | -- | -398/91 c | 7916 | 32788 107150 | 13115 7655 425161 55.5 | 1.334 % | c | 8016 | 32788 107150 | 14426 7755 430451 55.5 | 1.338 % | c | 8169 | 32788 107150 | 15869 7908 437395 55.3 | 1.338 % | c | 8394 | 32788 107150 | 17456 8133 446890 54.9 | 1.338 % | c ============================================================================== c (current CPU-time: 16.6185 s) c ============================================================================== c [1mFound solution: 856[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 8432 | 33005 107921 | 9901 8171 449855 55.1 | 1.338 % | c -- subsuming c -- var.elim.: 546/546 c -- var.elim.: 350/350 c | 8432 | 32810 107942 | -- 8171 -- -- | -- | -195/22 c | 8432 | 32810 107942 | 13124 8171 449855 55.1 | 1.338 % | c | 8533 | 32810 107942 | 14436 8272 453218 54.8 | 1.351 % | c | 8684 | 32810 107942 | 15880 8423 465060 55.2 | 1.351 % | c | 8910 | 32810 107942 | 17468 8649 492841 57.0 | 1.351 % | c | 9250 | 32810 107942 | 19214 8989 503086 56.0 | 1.351 % | c | 9759 | 32544 105545 | 20964 9484 547927 57.8 | 1.716 % | c | 10518 | 32544 105545 | 23061 10243 593641 58.0 | 1.716 % | c | 11658 | 32544 105545 | 25367 11383 744362 65.4 | 1.716 % | c | 13366 | 32544 105545 | 27904 13091 958359 73.2 | 1.716 % | c | 15928 | 32544 105545 | 30694 15653 1046663 66.9 | 1.716 % | c | 19775 | 32544 105545 | 33764 19500 1536427 78.8 | 1.716 % | c ============================================================================== c (current CPU-time: 43.6214 s) c ============================================================================== c [1mFound solution: 850[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 3 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 20542 | 32358 104726 | 9707 19855 1579857 79.6 | 1.716 % | c -- subsuming c -- var.elim.: 1000/1064 c -- var.elim.: 1064/1064 c -- var.elim.: 860/860 c -- var.elim.: 9/9 c -- subsuming c -- var.elim.: 539/539 c -- var.elim.: 44/44 c | 20542 | 32062 105158 | -- 19855 -- -- | -- | -294/437 c | 20542 | 32062 105158 | 12824 14684 652868 44.5 | 1.716 % | c | 20644 | 32062 105158 | 14107 7994 324602 40.6 | 2.497 % | c | 20796 | 32062 105158 | 15518 8146 327699 40.2 | 2.497 % | c ============================================================================== c (current CPU-time: 45.0631 s) c ============================================================================== c [1mFound solution: 783[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 20799 | 32249 105745 | 9674 8149 327724 40.2 | 2.497 % | c -- subsuming c -- var.elim.: 383/383 c -- var.elim.: 251/251 c | 20799 | 32153 105914 | -- 8149 -- -- | -- | -96/170 c | 20799 | 32153 105914 | 12861 8149 327724 40.2 | 2.497 % | c ============================================================================== c (current CPU-time: 45.3631 s) c ============================================================================== c [1mFound solution: 741[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 3 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 20802 | 32210 106194 | 9662 8152 327886 40.2 | 2.497 % | c -- subsuming c -- var.elim.: 220/220 c -- var.elim.: 182/182 c | 20802 | 32180 106479 | -- 8152 -- -- | -- | -30/286 c | 20802 | 32180 106479 | 12872 8152 327886 40.2 | 2.497 % | c ============================================================================== c (current CPU-time: 45.6171 s) c ============================================================================== c [1mFound solution: 732[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 3 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 20810 | 32224 106731 | 9667 8160 328436 40.2 | 2.497 % | c -- subsuming c -- var.elim.: 207/207 c -- var.elim.: 176/176 c | 20810 | 32198 106926 | -- 8160 -- -- | -- | -26/196 c | 20810 | 32198 106926 | 12879 8160 328436 40.2 | 2.497 % | c | 20910 | 32198 106926 | 14167 8260 333148 40.3 | 2.527 % | c | 21063 | 32198 106926 | 15583 8413 345697 41.1 | 2.527 % | c | 21288 | 32198 106926 | 17142 8638 368787 42.7 | 2.527 % | c | 21625 | 32198 106926 | 18856 8975 388123 43.2 | 2.527 % | c | 22132 | 32198 106926 | 20742 9482 431654 45.5 | 2.527 % | c | 22891 | 32198 106926 | 22816 10241 540663 52.8 | 2.527 % | c | 24030 | 32198 106926 | 25097 11380 665008 58.4 | 2.526 % | c ============================================================================== c (current CPU-time: 57.2153 s) c ============================================================================== c [1mFound solution: 712[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 3 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 25126 | 32221 107085 | 9666 12476 853144 68.4 | 2.526 % | c -- subsuming c -- var.elim.: 187/187 c -- var.elim.: 119/119 c | 25126 | 32208 107109 | -- 12476 -- -- | -- | -13/25 c | 25126 | 32208 107109 | 12883 12476 853144 68.4 | 2.526 % | c | 25227 | 32208 107109 | 14171 12577 863936 68.7 | 2.539 % | c | 25378 | 32208 107109 | 15588 12728 880191 69.2 | 2.539 % | c | 25605 | 32208 107109 | 17147 12955 907576 70.1 | 2.539 % | c | 25947 | 32208 107109 | 18862 13297 936754 70.4 | 2.539 % | c | 26453 | 32208 107109 | 20748 13803 1008801 73.1 | 2.539 % | c | 27212 | 32208 107109 | 22823 14562 1106717 76.0 | 2.539 % | c | 28354 | 32208 107109 | 25105 15704 1323279 84.3 | 2.539 % | c | 30062 | 32208 107109 | 27616 17412 1688803 97.0 | 2.539 % | c | 32624 | 32208 107109 | 30377 19974 2105718 105.4 | 2.539 % | c | 36469 | 32208 107109 | 33415 23819 2845004 119.4 | 2.539 % | c ============================================================================== c (current CPU-time: 112.005 s) c ============================================================================== c [1mFound solution: 696[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 3 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | 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.88 0.95 0.90 2/54 24262 Raw data (stat): 24262 (runsolver) R 24261 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422107686 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.90 0.95 0.90 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 2664 0 0 0 988 9 0 0 25 0 1 0 422107686 11689984 2349 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2854 2349 603 41 0 2813 0 vsize: 11416 [startup+20.0006 s] Raw data (loadavg): 0.92 0.96 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 3610 0 0 0 1984 13 0 0 25 0 1 0 422107686 14237696 2963 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3476 2963 603 41 0 3435 0 vsize: 13904 [startup+30.002 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 3914 0 0 0 2983 14 0 0 25 0 1 0 422107686 15421440 3267 4294967295 134512640 134672761 3221224576 3221223760 134615698 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3765 3267 603 41 0 3724 0 vsize: 15060 [startup+40.0024 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 4411 0 0 0 3981 16 0 0 25 0 1 0 422107686 17584128 3764 4294967295 134512640 134672761 3221224576 3221223760 134615686 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4293 3764 603 41 0 4252 0 vsize: 17172 [startup+50.0025 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 5934 0 0 0 4975 22 0 0 25 0 1 0 422107686 18505728 4026 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4518 4026 603 41 0 4477 0 vsize: 18072 [startup+60.0031 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 6301 0 0 0 5973 24 0 0 25 0 1 0 422107686 19320832 4217 4294967295 134512640 134672761 3221224576 3221223712 134614753 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4717 4217 603 41 0 4676 0 vsize: 18868 [startup+70.0035 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 6301 0 0 0 6974 24 0 0 25 0 1 0 422107686 19320832 4217 4294967295 134512640 134672761 3221224576 3221223616 134612927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4717 4217 603 41 0 4676 0 vsize: 18868 [startup+80.0045 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 6565 0 0 0 7973 24 0 0 25 0 1 0 422107686 20381696 4481 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4976 4481 603 41 0 4935 0 vsize: 19904 [startup+90.0052 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 7035 0 0 0 8973 25 0 0 25 0 1 0 422107686 22372352 4951 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5462 4951 603 41 0 5421 0 vsize: 21848 [startup+100.005 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 7589 0 0 0 9971 27 0 0 25 0 1 0 422107686 24612864 5505 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6009 5505 603 41 0 5968 0 vsize: 24036 [startup+110.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8073 0 0 0 10970 28 0 0 25 0 1 0 422107686 26587136 5989 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6491 5989 603 41 0 6450 0 vsize: 25964 [startup+120.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8697 0 0 0 11967 31 0 0 25 0 1 0 422107686 28393472 6437 4294967295 134512640 134672761 3221224576 3221223776 134610667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6932 6437 603 41 0 6891 0 vsize: 27728 [startup+130.006 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8697 0 0 0 12967 31 0 0 25 0 1 0 422107686 28393472 6437 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6932 6437 603 41 0 6891 0 vsize: 27728 [startup+140.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8697 0 0 0 13968 31 0 0 25 0 1 0 422107686 28393472 6437 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6932 6437 603 41 0 6891 0 vsize: 27728 [startup+150.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8697 0 0 0 14968 31 0 0 25 0 1 0 422107686 28393472 6437 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6932 6437 603 41 0 6891 0 vsize: 27728 [startup+160.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8697 0 0 0 15968 31 0 0 25 0 1 0 422107686 28393472 6437 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6932 6437 603 41 0 6891 0 vsize: 27728 [startup+170.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8698 0 0 0 16968 31 0 0 25 0 1 0 422107686 28393472 6438 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6932 6438 603 41 0 6891 0 vsize: 27728 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 8995 0 0 0 17968 32 0 0 25 0 1 0 422107686 29700096 6735 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7251 6735 603 41 0 7210 0 vsize: 29004 [startup+190.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 9487 0 0 0 18966 33 0 0 25 0 1 0 422107686 31674368 7227 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7733 7227 603 41 0 7692 0 vsize: 30932 [startup+200.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 9897 0 0 0 19966 34 0 0 25 0 1 0 422107686 33513472 7637 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8182 7637 603 41 0 8141 0 vsize: 32728 [startup+210.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 10349 0 0 0 20965 35 0 0 25 0 1 0 422107686 35364864 8089 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8634 8089 603 41 0 8593 0 vsize: 34536 [startup+220.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 10755 0 0 0 21964 36 0 0 25 0 1 0 422107686 36990976 8495 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9031 8495 603 41 0 8990 0 vsize: 36124 [startup+230.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11158 0 0 0 22963 38 0 0 25 0 1 0 422107686 38572032 8898 4294967295 134512640 134672761 3221224576 3221223760 134615921 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9417 8898 603 41 0 9376 0 vsize: 37668 [startup+240.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 23963 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9506 8993 603 41 0 9465 0 vsize: 38024 [startup+250.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 24963 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9506 8993 603 41 0 9465 0 vsize: 38024 [startup+260.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 25963 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9506 8993 603 41 0 9465 0 vsize: 38024 [startup+270.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 26963 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9506 8993 603 41 0 9465 0 vsize: 38024 [startup+280.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 27963 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9506 8993 603 41 0 9465 0 vsize: 38024 [startup+290.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 28964 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9506 8993 603 41 0 9465 0 vsize: 38024 [startup+300.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 29964 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9506 8993 603 41 0 9465 0 vsize: 38024 [startup+310.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 30964 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9506 8993 603 41 0 9465 0 vsize: 38024 [startup+320.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 31964 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9506 8993 603 41 0 9465 0 vsize: 38024 [startup+330.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11294 0 0 0 32964 38 0 0 25 0 1 0 422107686 38936576 8993 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9506 8993 603 41 0 9465 0 vsize: 38024 [startup+340.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 11640 0 0 0 33964 38 0 0 25 0 1 0 422107686 40390656 9339 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9861 9339 603 41 0 9820 0 vsize: 39444 [startup+350.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 12009 0 0 0 34963 39 0 0 25 0 1 0 422107686 41959424 9708 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10244 9708 603 41 0 10203 0 vsize: 40976 [startup+360.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 12389 0 0 0 35962 41 0 0 25 0 1 0 422107686 43528192 10088 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10627 10088 603 41 0 10586 0 vsize: 42508 [startup+370.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 12747 0 0 0 36962 42 0 0 25 0 1 0 422107686 44978176 10446 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10981 10446 603 41 0 10940 0 vsize: 43924 [startup+380.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13119 0 0 0 37960 43 0 0 25 0 1 0 422107686 46419968 10818 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11333 10818 603 41 0 11292 0 vsize: 45332 [startup+390.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13399 0 0 0 38960 44 0 0 25 0 1 0 422107686 47484928 11079 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11593 11079 603 41 0 11552 0 vsize: 46372 [startup+400.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13399 0 0 0 39960 44 0 0 25 0 1 0 422107686 47484928 11079 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11593 11079 603 41 0 11552 0 vsize: 46372 [startup+410.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13399 0 0 0 40960 44 0 0 25 0 1 0 422107686 47484928 11079 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11593 11079 603 41 0 11552 0 vsize: 46372 [startup+420.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13399 0 0 0 41961 44 0 0 25 0 1 0 422107686 47484928 11079 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11593 11079 603 41 0 11552 0 vsize: 46372 [startup+430.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13400 0 0 0 42961 44 0 0 25 0 1 0 422107686 47484928 11080 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11593 11080 603 41 0 11552 0 vsize: 46372 [startup+440.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13401 0 0 0 43961 44 0 0 25 0 1 0 422107686 47484928 11081 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11593 11081 603 41 0 11552 0 vsize: 46372 [startup+450.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13403 0 0 0 44961 44 0 0 25 0 1 0 422107686 47484928 11083 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11593 11083 603 41 0 11552 0 vsize: 46372 [startup+460.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13403 0 0 0 45961 44 0 0 25 0 1 0 422107686 47484928 11083 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11593 11083 603 41 0 11552 0 vsize: 46372 [startup+470.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13404 0 0 0 46972 44 0 0 25 0 1 0 422107686 47484928 11084 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11593 11084 603 41 0 11552 0 vsize: 46372 [startup+480.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13404 0 0 0 47972 44 0 0 25 0 1 0 422107686 47484928 11084 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11593 11084 603 41 0 11552 0 vsize: 46372 [startup+490.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13414 0 0 0 48972 44 0 0 25 0 1 0 422107686 47681536 11094 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11641 11094 603 41 0 11600 0 vsize: 46564 [startup+500.121 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13425 0 0 0 49972 44 0 0 25 0 1 0 422107686 47681536 11105 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11641 11105 603 41 0 11600 0 vsize: 46564 [startup+510.121 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13435 0 0 0 50973 44 0 0 25 0 1 0 422107686 47681536 11115 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11641 11115 603 41 0 11600 0 vsize: 46564 [startup+520.122 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13566 0 0 0 51972 44 0 0 25 0 1 0 422107686 48205824 11246 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11769 11246 603 41 0 11728 0 vsize: 47076 [startup+530.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 13963 0 0 0 52972 45 0 0 25 0 1 0 422107686 49909760 11643 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12185 11643 603 41 0 12144 0 vsize: 48740 [startup+540.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14301 0 0 0 53971 46 0 0 25 0 1 0 422107686 51220480 11981 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12505 11981 603 41 0 12464 0 vsize: 50020 [startup+550.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14546 0 0 0 54970 47 0 0 25 0 1 0 422107686 52092928 12172 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12172 603 41 0 12677 0 vsize: 50872 [startup+560.124 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14546 0 0 0 55971 47 0 0 25 0 1 0 422107686 52092928 12172 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12172 603 41 0 12677 0 vsize: 50872 [startup+570.124 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14546 0 0 0 56971 47 0 0 25 0 1 0 422107686 52092928 12172 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12172 603 41 0 12677 0 vsize: 50872 [startup+580.126 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14546 0 0 0 57971 47 0 0 25 0 1 0 422107686 52092928 12172 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12172 603 41 0 12677 0 vsize: 50872 [startup+590.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14546 0 0 0 58972 47 0 0 25 0 1 0 422107686 52092928 12172 4294967295 134512640 134672761 3221224576 3221223616 134612838 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12172 603 41 0 12677 0 vsize: 50872 [startup+600.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14547 0 0 0 59972 47 0 0 25 0 1 0 422107686 52092928 12173 4294967295 134512640 134672761 3221224576 3221223616 134613771 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12173 603 41 0 12677 0 vsize: 50872 [startup+610.136 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14547 0 0 0 60973 47 0 0 25 0 1 0 422107686 52092928 12173 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12173 603 41 0 12677 0 vsize: 50872 [startup+620.136 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 61973 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12175 603 41 0 12677 0 vsize: 50872 [startup+630.136 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 62973 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12175 603 41 0 12677 0 vsize: 50872 [startup+640.137 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 63973 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12175 603 41 0 12677 0 vsize: 50872 [startup+650.136 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 64974 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12175 603 41 0 12677 0 vsize: 50872 [startup+660.137 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 65974 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12175 603 41 0 12677 0 vsize: 50872 [startup+670.137 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 66974 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12175 603 41 0 12677 0 vsize: 50872 [startup+680.136 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 67974 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12175 603 41 0 12677 0 vsize: 50872 [startup+690.137 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 68974 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12175 603 41 0 12677 0 vsize: 50872 [startup+700.137 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14549 0 0 0 69974 47 0 0 25 0 1 0 422107686 52092928 12175 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12718 12175 603 41 0 12677 0 vsize: 50872 [startup+710.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 14841 0 0 0 70973 48 0 0 25 0 1 0 422107686 53420032 12467 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13042 12467 603 41 0 13001 0 vsize: 52168 [startup+720.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15143 0 0 0 71973 49 0 0 25 0 1 0 422107686 54685696 12769 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13351 12769 603 41 0 13310 0 vsize: 53404 [startup+730.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15485 0 0 0 72972 49 0 0 25 0 1 0 422107686 56123392 13111 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13702 13111 603 41 0 13661 0 vsize: 54808 [startup+740.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 73973 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13243 603 41 0 13762 0 vsize: 55212 [startup+750.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 74973 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223616 134613769 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13243 603 41 0 13762 0 vsize: 55212 [startup+760.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 75973 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13243 603 41 0 13762 0 vsize: 55212 [startup+770.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 76973 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223568 134565073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13243 603 41 0 13762 0 vsize: 55212 [startup+780.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 77973 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13243 603 41 0 13762 0 vsize: 55212 [startup+790.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 78973 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13243 603 41 0 13762 0 vsize: 55212 [startup+800.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 79974 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13243 603 41 0 13762 0 vsize: 55212 [startup+810.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 80974 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13243 603 41 0 13762 0 vsize: 55212 [startup+820.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 81974 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13243 603 41 0 13762 0 vsize: 55212 [startup+830.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 82974 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13243 603 41 0 13762 0 vsize: 55212 [startup+840.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 83974 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13243 603 41 0 13762 0 vsize: 55212 [startup+850.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15645 0 0 0 84974 50 0 0 25 0 1 0 422107686 56537088 13243 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13243 603 41 0 13762 0 vsize: 55212 [startup+860.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15646 0 0 0 85975 50 0 0 25 0 1 0 422107686 56537088 13244 4294967295 134512640 134672761 3221224576 3221223616 134612851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13244 603 41 0 13762 0 vsize: 55212 [startup+870.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15648 0 0 0 86975 50 0 0 25 0 1 0 422107686 56537088 13246 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13246 603 41 0 13762 0 vsize: 55212 [startup+880.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15649 0 0 0 87975 50 0 0 25 0 1 0 422107686 56537088 13247 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13247 603 41 0 13762 0 vsize: 55212 [startup+890.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15649 0 0 0 88975 50 0 0 25 0 1 0 422107686 56537088 13247 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13247 603 41 0 13762 0 vsize: 55212 [startup+900.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15649 0 0 0 89975 50 0 0 25 0 1 0 422107686 56537088 13247 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13247 603 41 0 13762 0 vsize: 55212 [startup+910.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15649 0 0 0 90976 50 0 0 25 0 1 0 422107686 56537088 13247 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13247 603 41 0 13762 0 vsize: 55212 [startup+920.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15649 0 0 0 91976 50 0 0 25 0 1 0 422107686 56537088 13247 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13803 13247 603 41 0 13762 0 vsize: 55212 [startup+930.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 15842 0 0 0 92975 50 0 0 25 0 1 0 422107686 57327616 13440 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13996 13440 603 41 0 13955 0 vsize: 55984 [startup+940.141 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 93975 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615611 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+950.141 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 94975 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+960.142 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 95975 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+970.141 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 96975 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+980.141 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 97976 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+990.142 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 98976 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1000.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 99976 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223776 134610642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1010.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 100976 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1020.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 101976 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1030.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 102977 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1040.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 103977 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1050.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 104977 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1060.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 105977 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1070.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 106977 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1080.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 107978 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1090.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 108978 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1100.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 109978 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1110.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 110978 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1120.15 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16190 0 0 0 111978 51 0 0 25 0 1 0 422107686 58507264 13729 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13729 603 41 0 14243 0 vsize: 57136 [startup+1130.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16192 0 0 0 112978 51 0 0 25 0 1 0 422107686 58507264 13731 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13731 603 41 0 14243 0 vsize: 57136 [startup+1140.15 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16194 0 0 0 113979 51 0 0 25 0 1 0 422107686 58507264 13733 4294967295 134512640 134672761 3221224576 3221223760 134615951 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14284 13733 603 41 0 14243 0 vsize: 57136 [startup+1150.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16445 0 0 0 114978 51 0 0 25 0 1 0 422107686 59817984 13984 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14604 13984 603 41 0 14563 0 vsize: 58416 [startup+1160.15 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16668 0 0 0 115978 52 0 0 25 0 1 0 422107686 60276736 14110 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14716 14110 603 41 0 14675 0 vsize: 58864 [startup+1170.15 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16668 0 0 0 116979 52 0 0 25 0 1 0 422107686 60276736 14110 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14716 14110 603 41 0 14675 0 vsize: 58864 [startup+1180.15 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16668 0 0 0 117979 52 0 0 25 0 1 0 422107686 60276736 14110 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14716 14110 603 41 0 14675 0 vsize: 58864 [startup+1190.15 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16668 0 0 0 118979 52 0 0 25 0 1 0 422107686 60276736 14110 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14716 14110 603 41 0 14675 0 vsize: 58864 [startup+1200.15 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 24262 Raw data (stat): 24262 (minisat+) R 24261 20937 20936 0 -1 0 16668 0 0 0 119979 52 0 0 25 0 1 0 422107686 60276736 14110 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14716 14110 603 41 0 14675 0 vsize: 58864 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.18 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 24262 Raw data (stat): 24262 (minisat+) Z 24261 20937 20936 0 -1 12 16669 0 0 0 119979 54 0 0 25 0 1 0 422107686 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.18 CPU time (s): 1200.35 CPU user time (s): 1199.8 CPU system time (s): 0.549916 CPU usage (%): 100.014 Max. virtual memory (Kb): 58864 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####