Name | normalized-opb/submitted/manquinho/logic-synthesis/normalized-e64.b.opb |
MD5SUM | bf7f8537c6faa135d25c67c53576abb5 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 49 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 608 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 608 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 608 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.03484 |
Number of variables | 607 |
Total number of constraints | 1053 |
Number of constraints which are clauses | 1022 |
Number of constraints which are cardinality constraints (but not clauses) | 31 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 3 |
Maximum length of a constraint | 32 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc2 THE 2005-04-13 20:29:29 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=590 boxname=wulflinc2 idbench=66 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: bf7f8537c6faa135d25c67c53576abb5 /oldhome/oroussel/tmp/wulflinc2/normalized-e64.b.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc2/normalized-e64.b.opb IDLAUNCH: 590 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 912812 kB Buffers: 33188 kB Cached: 68468 kB SwapCached: 4 kB Active: 53292 kB Inactive: 51184 kB HighTotal: 131008 kB HighFree: 58800 kB LowTotal: 903652 kB LowFree: 854012 kB SwapTotal: 2097136 kB SwapFree: 2097132 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6916 kB Slab: 11888 kB Committed_AS: 71676 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-13 20:49:31 (client local time) WITH STATUS 10 IN 1200.21 SECONDS stats: 590 7 1200.21 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 1022 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 | 1022 8200 | 340 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 82[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:27428 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1 | 32888 82605 | 10962 1 16 16.0 | 0.000 % | c | 101 | 32731 82280 | 12058 94 1328 14.1 | 0.441 % | c | 251 | 32731 82280 | 13264 244 4888 20.0 | 0.441 % | c | 476 | 32693 82200 | 14590 467 9207 19.7 | 0.538 % | c | 815 | 32655 82120 | 16049 805 14538 18.1 | 0.636 % | c ============================================================================== c [1mFound solution: 64[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1118 | 32544 81867 | 10848 1108 20015 18.1 | 0.636 % | c | 1219 | 32544 81867 | 11932 1209 21890 18.1 | 1.342 % | c | 1371 | 32544 81867 | 13126 1361 27251 20.0 | 1.342 % | c | 1597 | 32544 81867 | 14438 1587 32001 20.2 | 1.342 % | c | 1935 | 32544 81867 | 15882 1925 44062 22.9 | 1.342 % | c | 2442 | 32526 81825 | 17470 2426 58440 24.1 | 1.397 % | c | 3201 | 32524 81821 | 19217 3182 81772 25.7 | 1.402 % | c | 4340 | 32524 81821 | 21139 4321 124438 28.8 | 1.402 % | c | 6049 | 32524 81821 | 23253 6030 236669 39.2 | 1.402 % | c | 8611 | 32524 81821 | 25579 8592 404633 47.1 | 1.402 % | c | 12456 | 32524 81821 | 28136 12437 881628 70.9 | 1.402 % | c ============================================================================== c [1mFound solution: 57[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17530 | 32583 81971 | 10861 17511 1261267 72.0 | 1.402 % | c | 17631 | 32583 81971 | 11947 8857 728551 82.3 | 1.404 % | c | 17781 | 32557 81915 | 13141 9005 733381 81.4 | 1.474 % | c | 18007 | 32557 81915 | 14455 9231 741448 80.3 | 1.474 % | c | 18344 | 32557 81915 | 15901 9568 749366 78.3 | 1.474 % | c | 18850 | 32557 81915 | 17491 10074 785392 78.0 | 1.474 % | c | 19609 | 32557 81915 | 19240 10833 859333 79.3 | 1.474 % | c | 20748 | 32557 81915 | 21165 11972 919844 76.8 | 1.474 % | c | 22458 | 32557 81915 | 23281 13682 1056358 77.2 | 1.474 % | c | 25020 | 32557 81915 | 25609 16244 1287855 79.3 | 1.474 % | c ============================================================================== c [1mFound solution: 55[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25537 | 32576 81969 | 10858 16761 1329272 79.3 | 1.474 % | c | 25637 | 32576 81969 | 11943 8481 589547 69.5 | 1.477 % | c | 25787 | 32576 81969 | 13138 8631 595037 68.9 | 1.477 % | c | 26012 | 32576 81969 | 14451 8856 607205 68.6 | 1.477 % | c | 26349 | 32576 81969 | 15897 9193 625383 68.0 | 1.477 % | c | 26855 | 32576 81969 | 17486 9699 645599 66.6 | 1.477 % | c | 27616 | 32576 81969 | 19235 10460 688721 65.8 | 1.477 % | c | 28755 | 32576 81969 | 21159 11599 760883 65.6 | 1.477 % | c | 30463 | 32576 81969 | 23275 13307 926598 69.6 | 1.477 % | c | 33026 | 32576 81969 | 25602 15870 1052589 66.3 | 1.477 % | c | 36872 | 32576 81969 | 28162 19716 1313125 66.6 | 1.477 % | c | 42638 | 32540 81893 | 30979 25472 1707177 67.0 | 1.570 % | c | 51288 | 32540 81893 | 34077 13453 850735 63.2 | 1.570 % | c | 64262 | 32540 81893 | 37484 26427 1854535 70.2 | 1.570 % | c ============================================================================== c [1mFound solution: 53[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 71120 | 32558 81945 | 10852 33285 2473346 74.3 | 1.570 % | c | 71222 | 32558 81945 | 11937 6680 548160 82.1 | 1.583 % | c | 71372 | 32558 81945 | 13130 6830 551418 80.7 | 1.583 % | c | 71597 | 32558 81945 | 14444 7055 563546 79.9 | 1.583 % | c | 71934 | 32558 81945 | 15888 7392 572407 77.4 | 1.583 % | c | 72440 | 32558 81945 | 17477 7898 589289 74.6 | 1.583 % | c | 73199 | 32558 81945 | 19224 8657 630654 72.8 | 1.583 % | c | 74340 | 32558 81945 | 21147 9798 684750 69.9 | 1.583 % | c | 76048 | 32558 81945 | 23262 11506 842785 73.2 | 1.583 % | c | 78611 | 32558 81945 | 25588 14069 1080790 76.8 | 1.583 % | c | 82457 | 32558 81945 | 28147 17915 1447445 80.8 | 1.583 % | c | 88223 | 32558 81945 | 30962 23681 1883985 79.6 | 1.583 % | c | 96872 | 32558 81945 | 34058 32330 2567295 79.4 | 1.583 % | c | 109848 | 32558 81945 | 37464 21298 1707483 80.2 | 1.583 % | c | 129309 | 32558 81945 | 41210 13470 1145174 85.0 | 1.583 % | c | 158501 | 32558 81945 | 45331 42662 3823977 89.6 | 1.583 % | c | 202290 | 32558 81945 | 49864 18699 1418328 75.9 | 1.583 % | c | 267976 | 32558 81945 | 54851 46288 3760997 81.3 | 1.583 % | c | 366502 | 32558 81945 | 60336 17595 1604710 91.2 | 1.583 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.85 0.97 0.91 2/54 22589 Raw data (stat): 22589 (runsolver) R 22588 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420618846 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99983 s] Raw data (loadavg): 0.87 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 2487 0 0 0 990 7 0 0 25 0 1 0 420618846 12369920 2400 4294967295 134512640 134672761 3221224640 3221223808 134560785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3020 2400 603 41 0 2979 0 vsize: 12080 [startup+20.0008 s] Raw data (loadavg): 0.89 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 3085 0 0 0 1987 10 0 0 25 0 1 0 420618846 14782464 2998 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3609 2998 603 41 0 3568 0 vsize: 14436 [startup+30.0014 s] Raw data (loadavg): 0.91 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 3479 0 0 0 2986 12 0 0 25 0 1 0 420618846 16367616 3392 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3996 3392 603 41 0 3955 0 vsize: 15984 [startup+40.0019 s] Raw data (loadavg): 0.92 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 3479 0 0 0 3986 12 0 0 25 0 1 0 420618846 16367616 3392 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3996 3392 603 41 0 3955 0 vsize: 15984 [startup+50.0029 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 3591 0 0 0 4985 12 0 0 25 0 1 0 420618846 16896000 3504 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4125 3504 603 41 0 4084 0 vsize: 16500 [startup+60.0023 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 3592 0 0 0 5986 12 0 0 25 0 1 0 420618846 16896000 3505 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4125 3505 603 41 0 4084 0 vsize: 16500 [startup+70.003 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4021 0 0 0 6983 14 0 0 25 0 1 0 420618846 18644992 3934 4294967295 134512640 134672761 3221224640 3221223776 134560697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4552 3934 603 41 0 4511 0 vsize: 18208 [startup+80.003 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4372 0 0 0 7982 16 0 0 25 0 1 0 420618846 19988480 4285 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4880 4285 603 41 0 4839 0 vsize: 19520 [startup+90.0034 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4716 0 0 0 8980 17 0 0 25 0 1 0 420618846 21585920 4629 4294967295 134512640 134672761 3221224640 3221223632 134565768 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5270 4629 603 41 0 5229 0 vsize: 21080 [startup+100.003 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4716 0 0 0 9980 17 0 0 25 0 1 0 420618846 21585920 4629 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5270 4629 603 41 0 5229 0 vsize: 21080 [startup+110.003 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4716 0 0 0 10981 17 0 0 25 0 1 0 420618846 21585920 4629 4294967295 134512640 134672761 3221224640 3221223764 134566075 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5270 4629 603 41 0 5229 0 vsize: 21080 [startup+120.003 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4716 0 0 0 11981 17 0 0 25 0 1 0 420618846 21585920 4629 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5270 4629 603 41 0 5229 0 vsize: 21080 [startup+130.003 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4983 0 0 0 12980 19 0 0 25 0 1 0 420618846 22654976 4896 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5531 4896 603 41 0 5490 0 vsize: 22124 [startup+140.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5029 0 0 0 13980 19 0 0 25 0 1 0 420618846 22859776 4942 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5581 4942 603 41 0 5540 0 vsize: 22324 [startup+150.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5029 0 0 0 14980 19 0 0 25 0 1 0 420618846 22859776 4942 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5581 4942 603 41 0 5540 0 vsize: 22324 [startup+160.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5029 0 0 0 15980 19 0 0 25 0 1 0 420618846 22859776 4942 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5581 4942 603 41 0 5540 0 vsize: 22324 [startup+170.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5029 0 0 0 16980 19 0 0 25 0 1 0 420618846 22859776 4942 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5581 4942 603 41 0 5540 0 vsize: 22324 [startup+180.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5230 0 0 0 17980 19 0 0 25 0 1 0 420618846 23674880 5143 4294967295 134512640 134672761 3221224640 3221223840 134557811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5780 5143 603 41 0 5739 0 vsize: 23120 [startup+190.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5639 0 0 0 18979 21 0 0 25 0 1 0 420618846 25296896 5552 4294967295 134512640 134672761 3221224640 3221223808 134561391 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6176 5552 603 41 0 6135 0 vsize: 24704 [startup+200.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5639 0 0 0 19979 21 0 0 25 0 1 0 420618846 25296896 5552 4294967295 134512640 134672761 3221224640 3221223824 134559559 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6176 5552 603 41 0 6135 0 vsize: 24704 [startup+210.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5639 0 0 0 20979 21 0 0 25 0 1 0 420618846 25296896 5552 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6176 5552 603 41 0 6135 0 vsize: 24704 [startup+220.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5639 0 0 0 21979 21 0 0 25 0 1 0 420618846 25296896 5552 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6176 5552 603 41 0 6135 0 vsize: 24704 [startup+230.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5639 0 0 0 22980 21 0 0 25 0 1 0 420618846 25296896 5552 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6176 5552 603 41 0 6135 0 vsize: 24704 [startup+240.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5917 0 0 0 23979 22 0 0 25 0 1 0 420618846 26501120 5830 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6470 5830 603 41 0 6429 0 vsize: 25880 [startup+250.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6214 0 0 0 24977 23 0 0 25 0 1 0 420618846 27717632 6127 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6767 6127 603 41 0 6726 0 vsize: 27068 [startup+260.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6214 0 0 0 25977 23 0 0 25 0 1 0 420618846 27717632 6127 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6767 6127 603 41 0 6726 0 vsize: 27068 [startup+270.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6214 0 0 0 26978 23 0 0 25 0 1 0 420618846 27717632 6127 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6767 6127 603 41 0 6726 0 vsize: 27068 [startup+280.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6214 0 0 0 27978 23 0 0 25 0 1 0 420618846 27717632 6127 4294967295 134512640 134672761 3221224640 3221223776 134560703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6767 6127 603 41 0 6726 0 vsize: 27068 [startup+290.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6214 0 0 0 28978 23 0 0 25 0 1 0 420618846 27717632 6127 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6767 6127 603 41 0 6726 0 vsize: 27068 [startup+300.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6214 0 0 0 29978 23 0 0 25 0 1 0 420618846 27717632 6127 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6767 6127 603 41 0 6726 0 vsize: 27068 [startup+310.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6501 0 0 0 30978 24 0 0 25 0 1 0 420618846 28930048 6414 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7063 6414 603 41 0 7022 0 vsize: 28252 [startup+320.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6888 0 0 0 31977 25 0 0 25 0 1 0 420618846 30408704 6801 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7424 6801 603 41 0 7383 0 vsize: 29696 [startup+330.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7253 0 0 0 32976 26 0 0 25 0 1 0 420618846 32018432 7166 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7817 7166 603 41 0 7776 0 vsize: 31268 [startup+340.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7354 0 0 0 33976 26 0 0 25 0 1 0 420618846 32419840 7267 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7915 7267 603 41 0 7874 0 vsize: 31660 [startup+350.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7354 0 0 0 34976 26 0 0 25 0 1 0 420618846 32419840 7267 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7915 7267 603 41 0 7874 0 vsize: 31660 [startup+360.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7354 0 0 0 35977 26 0 0 25 0 1 0 420618846 32419840 7267 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7915 7267 603 41 0 7874 0 vsize: 31660 [startup+370.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7354 0 0 0 36977 26 0 0 25 0 1 0 420618846 32419840 7267 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7915 7267 603 41 0 7874 0 vsize: 31660 [startup+380.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7363 0 0 0 37977 26 0 0 25 0 1 0 420618846 32419840 7276 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7915 7276 603 41 0 7874 0 vsize: 31660 [startup+390.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7365 0 0 0 38977 26 0 0 25 0 1 0 420618846 32419840 7278 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7915 7278 603 41 0 7874 0 vsize: 31660 [startup+400.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7366 0 0 0 39977 26 0 0 25 0 1 0 420618846 32419840 7279 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7915 7279 603 41 0 7874 0 vsize: 31660 [startup+410.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7379 0 0 0 40978 26 0 0 25 0 1 0 420618846 32563200 7292 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7950 7292 603 41 0 7909 0 vsize: 31800 [startup+420.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 41978 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7950 7305 603 41 0 7909 0 vsize: 31800 [startup+430.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 42978 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7950 7305 603 41 0 7909 0 vsize: 31800 [startup+440.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 43978 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7950 7305 603 41 0 7909 0 vsize: 31800 [startup+450.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 44978 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7950 7305 603 41 0 7909 0 vsize: 31800 [startup+460.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 45979 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223744 134560347 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7950 7305 603 41 0 7909 0 vsize: 31800 [startup+470.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 46979 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7950 7305 603 41 0 7909 0 vsize: 31800 [startup+480.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 47979 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7950 7305 603 41 0 7909 0 vsize: 31800 [startup+490.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 48979 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223744 134554910 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7950 7305 603 41 0 7909 0 vsize: 31800 [startup+500.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 49979 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223808 134561016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7950 7305 603 41 0 7909 0 vsize: 31800 [startup+510.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 50980 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7950 7305 603 41 0 7909 0 vsize: 31800 [startup+520.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7516 0 0 0 51979 27 0 0 25 0 1 0 420618846 33099776 7429 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8081 7429 603 41 0 8040 0 vsize: 32324 [startup+530.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7718 0 0 0 52979 27 0 0 25 0 1 0 420618846 33910784 7631 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8279 7631 603 41 0 8238 0 vsize: 33116 [startup+540.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7718 0 0 0 53979 27 0 0 25 0 1 0 420618846 33910784 7631 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8279 7631 603 41 0 8238 0 vsize: 33116 [startup+550.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7718 0 0 0 54979 27 0 0 25 0 1 0 420618846 33910784 7631 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8279 7631 603 41 0 8238 0 vsize: 33116 [startup+560.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7718 0 0 0 55980 27 0 0 25 0 1 0 420618846 33910784 7631 4294967295 134512640 134672761 3221224640 3221223824 134558360 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8279 7631 603 41 0 8238 0 vsize: 33116 [startup+570.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7724 0 0 0 56980 27 0 0 25 0 1 0 420618846 33910784 7637 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8279 7637 603 41 0 8238 0 vsize: 33116 [startup+580.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7730 0 0 0 57980 27 0 0 25 0 1 0 420618846 33910784 7643 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8279 7643 603 41 0 8238 0 vsize: 33116 [startup+590.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7730 0 0 0 58980 27 0 0 25 0 1 0 420618846 33910784 7643 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8279 7643 603 41 0 8238 0 vsize: 33116 [startup+600.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7730 0 0 0 59980 27 0 0 25 0 1 0 420618846 33910784 7643 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8279 7643 603 41 0 8238 0 vsize: 33116 [startup+610.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7730 0 0 0 60981 27 0 0 25 0 1 0 420618846 33910784 7643 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8279 7643 603 41 0 8238 0 vsize: 33116 [startup+620.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7730 0 0 0 61981 27 0 0 25 0 1 0 420618846 33910784 7643 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8279 7643 603 41 0 8238 0 vsize: 33116 [startup+630.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7731 0 0 0 62981 27 0 0 25 0 1 0 420618846 33910784 7644 4294967295 134512640 134672761 3221224640 3221223824 134558930 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8279 7644 603 41 0 8238 0 vsize: 33116 [startup+640.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7736 0 0 0 63981 27 0 0 25 0 1 0 420618846 34045952 7649 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8312 7649 603 41 0 8271 0 vsize: 33248 [startup+650.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7737 0 0 0 64981 28 0 0 25 0 1 0 420618846 34045952 7650 4294967295 134512640 134672761 3221224640 3221223824 134559330 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8312 7650 603 41 0 8271 0 vsize: 33248 [startup+660.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7788 0 0 0 65981 28 0 0 25 0 1 0 420618846 34181120 7701 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8345 7701 603 41 0 8304 0 vsize: 33380 [startup+670.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8037 0 0 0 66980 29 0 0 25 0 1 0 420618846 35250176 7950 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8606 7950 603 41 0 8565 0 vsize: 34424 [startup+680.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8283 0 0 0 67979 30 0 0 25 0 1 0 420618846 36184064 8196 4294967295 134512640 134672761 3221224640 3221223808 134561016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8834 8196 603 41 0 8793 0 vsize: 35336 [startup+690.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8307 0 0 0 68980 30 0 0 25 0 1 0 420618846 36315136 8220 4294967295 134512640 134672761 3221224640 3221223732 1075346528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8866 8220 603 41 0 8825 0 vsize: 35464 [startup+700.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8307 0 0 0 69980 30 0 0 25 0 1 0 420618846 36315136 8220 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8866 8220 603 41 0 8825 0 vsize: 35464 [startup+710.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8315 0 0 0 70980 30 0 0 25 0 1 0 420618846 36315136 8228 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8866 8228 603 41 0 8825 0 vsize: 35464 [startup+720.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8315 0 0 0 71980 30 0 0 25 0 1 0 420618846 36315136 8228 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8866 8228 603 41 0 8825 0 vsize: 35464 [startup+730.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8315 0 0 0 72980 30 0 0 25 0 1 0 420618846 36315136 8228 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8866 8228 603 41 0 8825 0 vsize: 35464 [startup+740.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8322 0 0 0 73980 30 0 0 25 0 1 0 420618846 36462592 8235 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8902 8235 603 41 0 8861 0 vsize: 35608 [startup+750.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8323 0 0 0 74981 30 0 0 25 0 1 0 420618846 36462592 8236 4294967295 134512640 134672761 3221224640 3221223824 134559182 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8902 8236 603 41 0 8861 0 vsize: 35608 [startup+760.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8329 0 0 0 75981 30 0 0 25 0 1 0 420618846 36462592 8242 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8902 8242 603 41 0 8861 0 vsize: 35608 [startup+770.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8329 0 0 0 76981 30 0 0 25 0 1 0 420618846 36462592 8242 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8902 8242 603 41 0 8861 0 vsize: 35608 [startup+780.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8329 0 0 0 77981 30 0 0 25 0 1 0 420618846 36462592 8242 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8902 8242 603 41 0 8861 0 vsize: 35608 [startup+790.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8341 0 0 0 78981 30 0 0 25 0 1 0 420618846 36462592 8254 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8902 8254 603 41 0 8861 0 vsize: 35608 [startup+800.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8489 0 0 0 79981 30 0 0 25 0 1 0 420618846 37150720 8402 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9070 8402 603 41 0 9029 0 vsize: 36280 [startup+810.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8741 0 0 0 80980 31 0 0 25 0 1 0 420618846 38219776 8654 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9331 8654 603 41 0 9290 0 vsize: 37324 [startup+820.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8991 0 0 0 81980 31 0 0 25 0 1 0 420618846 39161856 8904 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9561 8904 603 41 0 9520 0 vsize: 38244 [startup+830.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9044 0 0 0 82981 31 0 0 25 0 1 0 420618846 39428096 8957 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9626 8957 603 41 0 9585 0 vsize: 38504 [startup+840.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9044 0 0 0 83981 31 0 0 25 0 1 0 420618846 39428096 8957 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9626 8957 603 41 0 9585 0 vsize: 38504 [startup+850.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9054 0 0 0 84981 31 0 0 25 0 1 0 420618846 39428096 8967 4294967295 134512640 134672761 3221224640 3221223808 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9626 8967 603 41 0 9585 0 vsize: 38504 [startup+860.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9064 0 0 0 85981 31 0 0 25 0 1 0 420618846 39587840 8977 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9665 8977 603 41 0 9624 0 vsize: 38660 [startup+870.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9070 0 0 0 86982 31 0 0 25 0 1 0 420618846 39587840 8983 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9665 8983 603 41 0 9624 0 vsize: 38660 [startup+880.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9070 0 0 0 87982 31 0 0 25 0 1 0 420618846 39587840 8983 4294967295 134512640 134672761 3221224640 3221223824 134559345 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9665 8983 603 41 0 9624 0 vsize: 38660 [startup+890.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9070 0 0 0 88982 31 0 0 25 0 1 0 420618846 39587840 8983 4294967295 134512640 134672761 3221224640 3221223744 134560224 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9665 8983 603 41 0 9624 0 vsize: 38660 [startup+900.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9071 0 0 0 89982 31 0 0 25 0 1 0 420618846 39587840 8984 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9665 8984 603 41 0 9624 0 vsize: 38660 [startup+910.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9071 0 0 0 90982 31 0 0 25 0 1 0 420618846 39587840 8984 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9665 8984 603 41 0 9624 0 vsize: 38660 [startup+920.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9083 0 0 0 91983 31 0 0 25 0 1 0 420618846 39587840 8996 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9665 8996 603 41 0 9624 0 vsize: 38660 [startup+930.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9084 0 0 0 92983 31 0 0 25 0 1 0 420618846 39587840 8997 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9665 8997 603 41 0 9624 0 vsize: 38660 [startup+940.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9085 0 0 0 93983 31 0 0 25 0 1 0 420618846 39587840 8998 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9665 8998 603 41 0 9624 0 vsize: 38660 [startup+950.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9085 0 0 0 94983 31 0 0 25 0 1 0 420618846 39587840 8998 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9665 8998 603 41 0 9624 0 vsize: 38660 [startup+960.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9086 0 0 0 95983 31 0 0 25 0 1 0 420618846 39587840 8999 4294967295 134512640 134672761 3221224640 3221223840 134557814 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9665 8999 603 41 0 9624 0 vsize: 38660 [startup+970.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9087 0 0 0 96983 31 0 0 25 0 1 0 420618846 39587840 9000 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9665 9000 603 41 0 9624 0 vsize: 38660 [startup+980.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9281 0 0 0 97983 32 0 0 25 0 1 0 420618846 40407040 9194 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9865 9194 603 41 0 9824 0 vsize: 39460 [startup+990.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9429 0 0 0 98983 32 0 0 25 0 1 0 420618846 40947712 9342 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9997 9342 603 41 0 9956 0 vsize: 39988 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9429 0 0 0 99982 33 0 0 25 0 1 0 420618846 40947712 9342 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9997 9342 603 41 0 9956 0 vsize: 39988 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9429 0 0 0 100982 33 0 0 25 0 1 0 420618846 40947712 9342 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9997 9342 603 41 0 9956 0 vsize: 39988 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9429 0 0 0 101982 33 0 0 25 0 1 0 420618846 40947712 9342 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9997 9342 603 41 0 9956 0 vsize: 39988 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9429 0 0 0 102982 33 0 0 25 0 1 0 420618846 40947712 9342 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9997 9342 603 41 0 9956 0 vsize: 39988 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9429 0 0 0 103982 33 0 0 25 0 1 0 420618846 40947712 9342 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9997 9342 603 41 0 9956 0 vsize: 39988 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9430 0 0 0 104983 33 0 0 25 0 1 0 420618846 40947712 9343 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9997 9343 603 41 0 9956 0 vsize: 39988 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9430 0 0 0 105983 33 0 0 25 0 1 0 420618846 40947712 9343 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9997 9343 603 41 0 9956 0 vsize: 39988 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9431 0 0 0 106983 33 0 0 25 0 1 0 420618846 40947712 9344 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9997 9344 603 41 0 9956 0 vsize: 39988 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9431 0 0 0 107983 33 0 0 25 0 1 0 420618846 40947712 9344 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9997 9344 603 41 0 9956 0 vsize: 39988 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9431 0 0 0 108983 33 0 0 25 0 1 0 420618846 40947712 9344 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9997 9344 603 41 0 9956 0 vsize: 39988 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9431 0 0 0 109983 33 0 0 25 0 1 0 420618846 40947712 9344 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9997 9344 603 41 0 9956 0 vsize: 39988 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9431 0 0 0 110984 33 0 0 25 0 1 0 420618846 40947712 9344 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9997 9344 603 41 0 9956 0 vsize: 39988 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9440 0 0 0 111984 33 0 0 25 0 1 0 420618846 41144320 9353 4294967295 134512640 134672761 3221224640 3221223808 134561256 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10045 9353 603 41 0 10004 0 vsize: 40180 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9452 0 0 0 112984 33 0 0 25 0 1 0 420618846 41144320 9365 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10045 9365 603 41 0 10004 0 vsize: 40180 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9462 0 0 0 113984 33 0 0 25 0 1 0 420618846 41144320 9375 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10045 9375 603 41 0 10004 0 vsize: 40180 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9474 0 0 0 114984 33 0 0 25 0 1 0 420618846 41340928 9387 4294967295 134512640 134672761 3221224640 3221223808 134561264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10093 9387 603 41 0 10052 0 vsize: 40372 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9484 0 0 0 115985 33 0 0 25 0 1 0 420618846 41340928 9397 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10093 9397 603 41 0 10052 0 vsize: 40372 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9486 0 0 0 116985 33 0 0 25 0 1 0 420618846 41340928 9399 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10093 9399 603 41 0 10052 0 vsize: 40372 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9534 0 0 0 117985 33 0 0 25 0 1 0 420618846 41611264 9447 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10159 9447 603 41 0 10118 0 vsize: 40636 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9715 0 0 0 118984 33 0 0 25 0 1 0 420618846 42278912 9628 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10322 9628 603 41 0 10281 0 vsize: 41288 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22589 Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9941 0 0 0 119984 34 0 0 25 0 1 0 420618846 43216896 9854 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10551 9854 603 41 0 10510 0 vsize: 42204 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 22589 Raw data (stat): 22589 (minisat+) Z 22588 20937 20936 0 -1 12 9944 0 0 0 119984 36 0 0 25 0 1 0 420618846 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.05 CPU time (s): 1200.21 CPU user time (s): 1199.84 CPU system time (s): 0.365944 CPU usage (%): 100.013 Max. virtual memory (Kb): 42204 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####