Name | normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-my_adder.opb |
MD5SUM | fe8f615a95a6852516985b8e3e78bd85 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 4561 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 577 |
Biggest coefficient in the objective function | 61 |
Number of bits for the biggest coefficient in the objective function | 6 |
Sum of the numbers in the objective function | 24510 |
Number of bits of the sum of numbers in the objective function | 15 |
Biggest number in a constraint | 61 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 24510 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02584 |
Number of variables | 577 |
Total number of constraints | 1322 |
Number of constraints which are clauses | 1306 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 16 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 17 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc3 THE 2005-05-25 16:56:08 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=21837 boxname=wulflinc3 idbench=255 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: fe8f615a95a6852516985b8e3e78bd85 /oldhome/oroussel/tmp/wulflinc3/normalized-my_adder.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-my_adder.opb IDLAUNCH: 21837 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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: 772820 kB Buffers: 34936 kB Cached: 207280 kB SwapCached: 0 kB Active: 78976 kB Inactive: 165884 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 772568 kB SwapTotal: 2097136 kB SwapFree: 2096800 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6576 kB Slab: 11284 kB Committed_AS: 71792 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 17:16:38 (client local time) WITH STATUS 152 IN 1229.9 SECONDS stats: 21837 7 1229.9 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 1322 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1322 4977 | 440 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 6274[0m c ---[ 0]---> Sorter-cost:87831 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1 | 210130 492551 | 70043 1 7 7.0 | 0.000 % | c | 101 | 209639 491465 | 77047 98 1983 20.2 | 0.188 % | c | 251 | 209398 490919 | 84752 246 3047 12.4 | 0.270 % | c | 477 | 209398 490919 | 93227 472 5320 11.3 | 0.270 % | c | 814 | 209398 490919 | 102549 809 7426 9.2 | 0.270 % | c | 1320 | 209398 490919 | 112804 1315 12893 9.8 | 0.270 % | c | 2079 | 208099 487975 | 124085 2062 18966 9.2 | 0.850 % | c | 3223 | 207777 487250 | 136493 3203 75259 23.5 | 1.015 % | c | 4934 | 207777 487250 | 150143 4914 465375 94.7 | 1.015 % | c | 7496 | 207777 487250 | 165157 7476 523941 70.1 | 1.015 % | c | 11343 | 207124 485763 | 181673 11316 605974 53.6 | 1.304 % | c ============================================================================== c [1mFound solution: 6030[0m c ---[ 0]---> Sorter-cost:63107 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15902 | 341282 799222 | 113760 15812 677541 42.8 | 1.304 % | c | 16002 | 341282 799222 | 125136 15912 678586 42.6 | 1.292 % | c | 16153 | 341282 799222 | 137649 16063 680125 42.3 | 1.292 % | c | 16378 | 341282 799222 | 151414 16288 682659 41.9 | 1.292 % | c | 16715 | 341282 799222 | 166556 16625 686273 41.3 | 1.292 % | c | 17222 | 341282 799222 | 183211 17132 689710 40.3 | 1.292 % | c | 17982 | 341282 799222 | 201532 17892 701677 39.2 | 1.292 % | c ============================================================================== c [1mFound solution: 5941[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18575 | 341328 799730 | 113776 18485 726783 39.3 | 1.292 % | c | 18675 | 341311 799693 | 125153 18584 727472 39.1 | 1.297 % | c | 18825 | 341311 799693 | 137668 18734 728419 38.9 | 1.297 % | c | 19050 | 341311 799693 | 151435 18959 730280 38.5 | 1.297 % | c | 19388 | 341311 799693 | 166579 19297 732516 38.0 | 1.297 % | c | 19894 | 341311 799693 | 183237 19803 738567 37.3 | 1.297 % | c | 20653 | 341060 799139 | 201561 20560 748577 36.4 | 1.351 % | c | 21792 | 341060 799139 | 221717 21699 757149 34.9 | 1.351 % | c | 23500 | 341060 799139 | 243888 23407 808068 34.5 | 1.351 % | c | 26064 | 340058 796875 | 268277 25935 888362 34.3 | 1.591 % | c | 29909 | 340058 796875 | 295105 29780 993861 33.4 | 1.591 % | c | 35675 | 340058 796875 | 324616 35546 1611580 45.3 | 1.591 % | c | 44326 | 340058 796875 | 357077 44197 2011857 45.5 | 1.591 % | c | 57300 | 339999 796741 | 392785 57162 2368847 41.4 | 1.609 % | c | 76763 | 339999 796741 | 432064 76625 7374052 96.2 | 1.609 % | c | 105956 | 339999 796741 | 475270 105818 9897084 93.5 | 1.609 % | c ============================================================================== c [1mFound solution: 5700[0m c ---[ 0]---> Sorter-cost:64909 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 108372 | 479644 1122919 | 159881 108234 10027671 92.6 | 1.609 % | c | 108473 | 479644 1122919 | 175869 108335 10028620 92.6 | 1.141 % | c | 108623 | 479644 1122919 | 193456 108485 10030258 92.5 | 1.141 % | c | 108848 | 479644 1122919 | 212801 108710 10032710 92.3 | 1.141 % | c | 109185 | 479644 1122919 | 234081 109047 10045641 92.1 | 1.141 % | c | 109691 | 479498 1122590 | 257489 109542 10064209 91.9 | 1.162 % | c | 110451 | 479498 1122590 | 283238 110302 10074504 91.3 | 1.162 % | c | 111590 | 479498 1122590 | 311562 111441 10093566 90.6 | 1.162 % | c | 113298 | 479498 1122590 | 342719 113149 10108665 89.3 | 1.162 % | c | 115860 | 479488 1122570 | 376991 115708 10180504 88.0 | 1.165 % | c | 119704 | 479488 1122570 | 414690 119552 10487501 87.7 | 1.165 % | c | 125470 | 479488 1122570 | 456159 125318 11610478 92.6 | 1.165 % | c | 134119 | 479488 1122570 | 501775 133967 11828437 88.3 | 1.165 % | c | 147093 | 479488 1122570 | 551952 146941 12479339 84.9 | 1.165 % | c | 166556 | 479456 1122498 | 607147 166403 15031220 90.3 | 1.175 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 2628 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): 0.84 0.95 0.98 2/54 2624 Raw data (stat): 2624 (runsolver) R 2623 20224 20223 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 782258149 1052672 97 4294967295 134512640 135381576 3221224496 3221219936 134514522 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 97 215 215 0 42 0 vsize: 1028 [startup+10.0013 s] Raw data (loadavg): 0.87 0.95 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0016 s] Raw data (loadavg): 0.89 0.95 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0026 s] Raw data (loadavg): 0.90 0.95 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0035 s] Raw data (loadavg): 0.92 0.95 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.004 s] Raw data (loadavg): 0.93 0.96 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0041 s] Raw data (loadavg): 0.94 0.96 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.005 s] Raw data (loadavg): 0.95 0.96 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0055 s] Raw data (loadavg): 0.96 0.96 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0053 s] Raw data (loadavg): 0.96 0.96 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.005 s] Raw data (loadavg): 0.97 0.96 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.006 s] Raw data (loadavg): 0.97 0.96 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.006 s] Raw data (loadavg): 0.98 0.96 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.007 s] Raw data (loadavg): 0.98 0.96 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.007 s] Raw data (loadavg): 0.98 0.96 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.012 s] Raw data (loadavg): 0.98 0.97 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2628 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2681 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2681 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2681 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2681 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2681 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2681 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2683 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.04 s] Raw data (loadavg): 1.07 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.04 s] Raw data (loadavg): 1.06 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.04 s] Raw data (loadavg): 1.05 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.04 s] Raw data (loadavg): 1.04 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.04 s] Raw data (loadavg): 1.04 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.04 s] Raw data (loadavg): 1.03 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.041 s] Raw data (loadavg): 1.03 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.041 s] Raw data (loadavg): 1.02 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.042 s] Raw data (loadavg): 1.02 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.042 s] Raw data (loadavg): 1.01 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.042 s] Raw data (loadavg): 1.01 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.042 s] Raw data (loadavg): 1.01 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.042 s] Raw data (loadavg): 1.01 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.043 s] Raw data (loadavg): 1.01 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.04 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.04 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.04 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.04 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.04 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.04 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.04 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.04 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.04 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.05 s] Raw data (loadavg): 1.00 0.99 0.98 2/55 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.77 s] Raw data (loadavg): 1.00 0.99 0.98 1/53 2685 Raw data (stat): 2624 (minisat+_script) S 2623 20224 20223 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782258149 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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.9 CPU user time (s): 1228.93 CPU system time (s): 0.969852 CPU usage (%): 100.01 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####