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 wulflinc23 THE 2005-05-27 05:15:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23009 boxname=wulflinc23 idbench=255 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fe8f615a95a6852516985b8e3e78bd85 /oldhome/oroussel/tmp/wulflinc23/normalized-my_adder.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-my_adder.opb IDLAUNCH: 23009 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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 : 3 cpu MHz : 451.037 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: 458028 kB Buffers: 33840 kB Cached: 521052 kB SwapCached: 532 kB Active: 51788 kB Inactive: 505524 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 457776 kB SwapTotal: 2097136 kB SwapFree: 2096016 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5636 kB Slab: 13688 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-27 05:36:22 (client local time) WITH STATUS 152 IN 1229.89 SECONDS stats: 23009 7 1229.89 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: 27273 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.93 0.98 0.92 2/54 27269 Raw data (stat): 27269 (runsolver) R 27268 5562 5561 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853569357 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 0 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0004 s] Raw data (loadavg): 0.94 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0007 s] Raw data (loadavg): 0.95 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0011 s] Raw data (loadavg): 0.95 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.002 s] Raw data (loadavg): 0.96 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0027 s] Raw data (loadavg): 0.97 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.002 s] Raw data (loadavg): 0.97 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s] Raw data (loadavg): 0.97 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0036 s] Raw data (loadavg): 0.98 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.004 s] Raw data (loadavg): 0.98 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.004 s] Raw data (loadavg): 0.98 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.016 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.021 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.021 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.021 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.022 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.021 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.022 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.021 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.022 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.027 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.027 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.027 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.027 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.027 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.027 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.028 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.027 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.028 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.028 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.028 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.028 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.028 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.027 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.028 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.029 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.029 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.028 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.029 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.029 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.031 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.031 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.031 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.031 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.031 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.75 s] Raw data (loadavg): 0.99 0.98 0.92 1/53 27273 Raw data (stat): 27269 (minisat+_script) S 27268 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853569357 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.75 CPU time (s): 1229.89 CPU user time (s): 1228.9 CPU system time (s): 0.995848 CPU usage (%): 100.012 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####