Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare1_1.opb |
MD5SUM | 452acf9ed3adc2d2cfe293dad01c0934 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 167110 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 180 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 6442450938 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 536870912 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 6442450938 |
Number of bits of the biggest sum of numbers | 33 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.02 |
Number of variables | 280 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 45 |
Number of constraints which are nor clauses,nor cardinality constraints | 11 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 130 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc29 THE 2005-05-27 08:01:00 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23470 boxname=wulflinc29 idbench=1114 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 452acf9ed3adc2d2cfe293dad01c0934 /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-markshare1_1.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-markshare1_1.opb IDLAUNCH: 23470 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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: 911112 kB Buffers: 19616 kB Cached: 82408 kB SwapCached: 452 kB Active: 18640 kB Inactive: 85688 kB HighTotal: 131008 kB HighFree: 47488 kB LowTotal: 903652 kB LowFree: 863624 kB SwapTotal: 2097892 kB SwapFree: 2096760 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5616 kB Slab: 13508 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 08:21:29 (client local time) WITH STATUS 152 IN 1229.91 SECONDS stats: 23470 7 1229.91 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 17 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###### c -- Clauses(.)/Splits(s): (none) c ---[ 16]---> BDD-cost: 10 c ---[ 15]---> BDD-cost: 10 c ---[ 14]---> BDD-cost: 10 c ---[ 13]---> BDD-cost: 10 c ---[ 12]---> BDD-cost: 10 c ---[ 10]---> BDD-cost:87035 c ---[ 8]---> BDD-cost:82838 c ---[ 6]---> BDD-cost:89015 c ---[ 4]---> BDD-cost:39244 c ---[ 2]---> BDD-cost:62663 c ---[ 0]---> BDD-cost:60806 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1194561 3457768 | 398187 0 0 nan | 0.000 % | c | 100 | 1194469 3457584 | 438005 98 4658 47.5 | 0.026 % | c ============================================================================== c [1mFound solution: 6879072[0m c ---[ 0]---> Sorter-cost: 1725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 106 | 1198871 3467866 | 399623 104 13063 125.6 | 0.026 % | c ============================================================================== c [1mFound solution: 6534298[0m c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 107 | 1198906 3468005 | 399635 105 13109 124.8 | 0.026 % | c ============================================================================== c [1mFound solution: 6443290[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 107 | 1198926 3468050 | 399642 105 13109 124.8 | 0.026 % | c ============================================================================== c [1mFound solution: 6425568[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 117 | 1198942 3468088 | 399647 115 22668 197.1 | 0.026 % | c ============================================================================== c [1mFound solution: 3709466[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 118 | 1198972 3468158 | 399657 116 22718 195.8 | 0.026 % | c ============================================================================== c [1mFound solution: 3000667[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 121 | 1198994 3468212 | 399664 119 22816 191.7 | 0.026 % | c | 221 | 1198994 3468212 | 439630 219 29613 135.2 | 0.027 % | c | 372 | 1198994 3468212 | 483593 370 36880 99.7 | 0.027 % | c | 597 | 1198994 3468212 | 531952 595 45162 75.9 | 0.027 % | c | 934 | 1198994 3468212 | 585148 932 568779 610.3 | 0.027 % | c | 1440 | 1198994 3468212 | 643662 1438 829660 577.0 | 0.027 % | c | 2201 | 1198994 3468212 | 708029 2199 869139 395.2 | 0.027 % | c | 3340 | 1198994 3468212 | 778832 3338 948281 284.1 | 0.027 % | c ============================================================================== c [1mFound solution: 2998212[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3710 | 1199011 3468261 | 399670 3708 956775 258.0 | 0.027 % | c | 3814 | 1199011 3468261 | 439637 3812 1182763 310.3 | 0.028 % | c ============================================================================== c [1mFound solution: 2485433[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3888 | 1199029 3468310 | 399676 3886 1205452 310.2 | 0.028 % | c | 3988 | 1199029 3468310 | 439643 3986 1221539 306.5 | 0.028 % | c | 4139 | 1199029 3468310 | 483607 4137 1227535 296.7 | 0.028 % | c | 4364 | 1199029 3468310 | 531968 4362 1238676 284.0 | 0.028 % | c ============================================================================== c [1mFound solution: 2479423[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4438 | 1199053 3468367 | 399684 4436 1241960 280.0 | 0.028 % | c | 4538 | 1199053 3468367 | 439652 4536 1261631 278.1 | 0.028 % | c | 4689 | 1199053 3468367 | 483617 4687 1270123 271.0 | 0.028 % | c | 4914 | 1199053 3468367 | 531979 4912 1282886 261.2 | 0.028 % | c | 5253 | 1199053 3468367 | 585177 5251 1298710 247.3 | 0.028 % | c | 5759 | 1199053 3468367 | 643695 5757 1322349 229.7 | 0.028 % | c ============================================================================== c [1mFound solution: 2424683[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6105 | 1199065 3468403 | 399688 6103 1331830 218.2 | 0.028 % | c | 6206 | 1199065 3468403 | 439656 6204 1420161 228.9 | 0.028 % | c ============================================================================== c [1mFound solution: 2424593[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6303 | 1199082 3468449 | 399694 6301 1423998 226.0 | 0.028 % | c | 6405 | 1199082 3468449 | 439663 6403 1622195 253.3 | 0.029 % | c | 6560 | 1199082 3468449 | 483629 6558 1818046 277.2 | 0.029 % | c | 6789 | 1199082 3468449 | 531992 6787 1971496 290.5 | 0.029 % | c | 7127 | 1199082 3468449 | 585191 7125 1993412 279.8 | 0.029 % | c | 7634 | 1199082 3468449 | 643711 7632 2023817 265.2 | 0.029 % | c | 8393 | 1199082 3468449 | 708082 8391 2067658 246.4 | 0.029 % | c ============================================================================== c [1mFound solution: 2424372[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8765 | 1199096 3468488 | 399698 8763 2083215 237.7 | 0.029 % | c | 8868 | 1199096 3468488 | 439667 8866 2360292 266.2 | 0.029 % | c | 9018 | 1199096 3468488 | 483634 9016 2605265 289.0 | 0.029 % | c | 9245 | 1199096 3468488 | 531998 9243 2732022 295.6 | 0.029 % | c | 9584 | 1199096 3468488 | 585197 9582 2907460 303.4 | 0.029 % | c | 10091 | 1199096 3468488 | 643717 10089 2932346 290.6 | 0.029 % | c ============================================================================== c [1mFound solution: 2376660[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10272 | 1199115 3468534 | 399705 10270 2952657 287.5 | 0.029 % | c | 10373 | 1199115 3468534 | 439675 10371 2958298 285.2 | 0.029 % | c | 10525 | 1199115 3468534 | 483643 10523 2963903 281.7 | 0.029 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 13096 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### 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): 1.00 1.01 0.93 2/54 13092 Raw data (stat): 13092 (runsolver) R 13091 20001 20000 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854553408 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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+9.99997 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 13096 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0012 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 13096 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.002 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0012 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0022 s] Raw data (loadavg): 1.00 1.01 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0021 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0025 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0026 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0023 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.003 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.004 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.003 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.003 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.004 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.004 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.005 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.005 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.005 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.005 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.005 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.005 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.005 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.005 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.006 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.006 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.006 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.006 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.006 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.006 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13098 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.011 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.013 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.012 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.013 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.013 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.014 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.015 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.017 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.018 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.017 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.018 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.018 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.018 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.024 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.024 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.026 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.033 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.033 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.033 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.034 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.034 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.034 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.035 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.035 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.036 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.036 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.037 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.037 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.042 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.047 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.047 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.047 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.056 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.056 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.77 s] Raw data (loadavg): 1.00 1.00 0.93 1/53 13100 Raw data (stat): 13092 (minisat+_script) S 13091 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854553408 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.77 CPU time (s): 1229.91 CPU user time (s): 1228.82 CPU system time (s): 1.08783 CPU usage (%): 100.011 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####